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

```

#### ENVIRONMENTVARIABLES

```       ERGOLIB
Alternative path for the Alt-Ergo library

```

#### AUTHORS

```       Sylvain Conchon <conchon@lri.fr> and Evelyne Contejean <contejea@lri.fr>

```

#### SEEALSO

```       Alt-Ergo web site: http://alt-ergo.lri.fr

October, 2006                               Alt-Ergo(1)
```