Provided by:

alt-ergo_0.99.1+dfsg1-4build3_amd64 **NAME**

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

**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__
(C) 2006 -- 2013 Alt-Ergo(1)