Provided by: alt-ergo_0.94-1_amd64

**NAME**

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

**SYNOPSIS**

alt-ergo[options]files

**DESCRIPTION**

Alt-Ergois an automatic theorem prover. It takes as inputs an arbitrary polymorphic and multi-sorted first-order formula written is the Why's syntax.

**OPTIONS**

-hHelp. 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**

ERGOLIBAlternative path for the Alt-Ergo library

**AUTHORS**

SylvainConchon<conchon@lri.fr>andEvelyneContejean<contejea@lri.fr>

**SEE** **ALSO**

Alt-Ergowebsite:http://alt-ergo.lri.frOctober, 2006 Alt-Ergo(1)