NAMEAlt-Ergo - An automatic theorem prover dedicated to program verification
SYNOPSISalt-ergo [ options ] files
DESCRIPTIONAlt-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] 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. -pairs Theory of pairs. In order to use this theory, you should add the following prelude in your files: type 'a pair logic pair : 'a, 'a -> 'a pair logic fst: 'a pair -> 'a logic snd: 'a pair -> 'a
ENVIRONMENT VARIABLESERGOLIB Alternative path for the Alt-Ergo library
AUTHORSSylvain Conchon <firstname.lastname@example.org> and Evelyne Contejean <email@example.com>
SEE ALSOAlt-Ergo web site: //alt-ergo.lri.fr October, 2006 ALT-ERGO(1)