GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages


Manual Reference Pages  -  ALT-ERGO (1)

NAME

Alt-Ergo - An automatic theorem prover dedicated to program verification

CONTENTS

Synopsis
Description
Options
Examples
Environment Variables
Authors
See Also

SYNOPSIS

alt-ergo [ options ] file

DESCRIPTION

Alt-Ergo is an automatic theorem prover. It takes as inputs an arbitrary polymorphic and multi-sorted first-order formula written is a why like syntax.

OPTIONS

-h Help. Will give you the full list of command line options.

EXAMPLES

A theory of functional arrays with integer indexes . This theory provides a built-in type (’a,’b) farray and a built-in syntax for manipulating arrays.
 

For instance, given an abstract datatype tau and a functional array t of type (int, tau) farray declared as follows:

type tau

logic t : (int, tau) farray

The expressions:

t[i] denotes the value stored in t at index i

t[i1<-v1,...,in<-vn] denotes an array which stores the same values as t for every index except possibly i1,...,in, where it stores value v1,...,vn. This expression is equivalent to ((t[i1<-v1])[i2<-v2])...[in<-vn].

Examples.

t[0<-v][1<-w]

t[0<-v, 1<-w]

t[0<-v, 1<-w][1]

A theory of enumeration types.
 

For instance an enumeration type t with constructors A, B, C is defined as follows :

type t = A | B | C

Which means that all values of type t are equal to either A, B or C. And that all these constructors are distinct.

A theory of polymorphic records.
 

For instance a polymorphic record type ’a t with two labels a and b of type ’a and int respectively is defined as follows:

type ’a t = { a : ’a; b : int }

The expressions { a = 4; b = 5 } and { r with b = 3} denote records, while the dot notation r.a is used to access to labels.

Alt-Ergo (v. >= 0.95) allows the user to force the type of terms using the syntax <term> : <type>. The example below illustrates the use of this new feature.
 

type ’a list

logic nil : ’b list

logic f : ’c list -> int

goal g1 : f(nil) = f(nil) (* not valid because the two instances of nil may have different types *)

goal g2 : f(nil:’d list) = f(nil:’d list) (* valid *)

ENVIRONMENT VARIABLES

ERGOLIB
  Alternative path for the Alt-Ergo library

AUTHORS

Sylvain Conchon <conchon@lri.fr> and Evelyne Contejean <contejea@lri.fr>

SEE ALSO

Alt-Ergo web site: http://alt-ergo.lri.fr

Search for    or go to Top of page |  Section 1 |  Main Index


--> ALT-ERGO (1) (C) 2006 -- 2013

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with manServer 1.07.