xenial (1) alt-ergo.1.gz

Provided by: alt-ergo_0.99.1+dfsg1-4build3_amd64 bug

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)