NAME¶
Alt-Ergo - An automatic theorem prover dedicated to program verification
SYNOPSIS¶
alt-ergo [
options ]
files
DESCRIPTION¶
Alt-Ergo is an automatic theorem prover. It takes as inputs an arbitrary
polymorphic and multi-sorted first-order formula written is the Why's syntax.
OPTIONS¶
- -h
- Help. Will give you the full list of command line options.
- 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.
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
