Provided by: alt-ergo_1.30+dfsg1-1_amd64 bug


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


       alt-ergo [ options ] file


       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.


       -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].



              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 *)


              Alternative path for the Alt-Ergo library


       Sylvain Conchon <> and Evelyne Contejean <>


       Alt-Ergo web site:

                                         (C)  2006 -- 2013                            Alt-Ergo(1)