AltErgo  An automatic theorem prover dedicated to program verification
altergo [
options ]
file
AltErgo is an automatic theorem prover. It takes as inputs an arbitrary
polymorphic and multisorted firstorder formula written is a why like syntax.
 h
 Help. Will give you the full list of command line options.
 A theory of functional arrays with integer indexes . This
theory provides a builtin type ('a,'b) farray and a builtin 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.
 AltErgo (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 *)
 ERGOLIB
 Alternative path for the AltErgo library
Sylvain Conchon
<conchon@lri.fr> and Evelyne Contejean
<contejea@lri.fr>
AltErgo web site:
http://altergo.lri.fr