Homepage > Man Pages > Category > General Commands
Homepage > Man Pages > Name > A

# alt-ergo

## man page of alt-ergo

### alt-ergo: An automatic theorem prover dedicated to program verification

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

-pairs Theory of pairs. In order to use this theory, you should add the

type 'a pair

logic pair : 'a, 'a -> 'a pair

logic fst: 'a pair -> 'a

logic snd: 'a pair -> 'a

ENVIRONMENT VARIABLES
ERGOLIB
Alternative path for the Alt-Ergo library

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

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

October, 2006                     ALT-ERGO(1)
```

Contact · Imprint · Privacy

Page generated in 25.40ms.