1Alt-Ergo(1)                 General Commands Manual                Alt-Ergo(1)
2
3
4

NAME

6       Alt-Ergo  -  An automatic theorem prover dedicated to program verifica‐
7       tion
8
9
10

SYNOPSIS

12       alt-ergo [ options ] files
13
14
15

DESCRIPTION

17       Alt-Ergo is an automatic theorem prover.  It takes as inputs  an  arbi‐
18       trary  polymorphic  and multi-sorted first-order formula written is the
19       Why's syntax.
20
21

OPTIONS

23       -h     Help. Will give you the full list of command line options.
24
25
26       A theory of functional arrays with integer indexes . This theory
27              provides a built-in type ('a,'b) farray and  a  built-in  syntax
28              for manipulating arrays.
29
30              For  instance,  given  an abstract datatype tau and a functional
31              array t of type (int, tau) farray declared as follows:
32
33              type tau
34
35              logic t : (int, tau) farray
36
37              The expressions:
38
39              t[i] denotes the value stored in t at index i
40
41              t[i1<-v1,...,in<-vn] denotes an array which stores the same val‐
42              ues  as  t  for  every index except possibly i1,...,in, where it
43              stores  value  v1,...,vn.  This  expression  is  equivalent   to
44              ((t[i1<-v1])[i2<-v2])...[in<-vn].
45
46
47              Examples.
48
49              t[0<-v][1<-w]
50
51              t[0<-v, 1<-w]
52
53              t[0<-v, 1<-w][1]
54
55
56
57       A theory of enumeration types.
58
59              For  instance an enumeration type t with constructors A, B, C is
60              defined as follows :
61
62              type t = A | B | C
63
64              Which means that all values of type t are equal to either  A,  B
65              or C. And that all these constructors are distinct.
66
67
68
69       -pairs Theory of pairs. In order to use this theory, you should add the
70              following prelude in your files:
71
72              type 'a pair
73
74              logic pair : 'a, 'a -> 'a pair
75
76              logic fst: 'a pair -> 'a
77
78              logic snd: 'a pair -> 'a
79
80
81

ENVIRONMENT VARIABLES

83       ERGOLIB
84              Alternative path for the Alt-Ergo library
85
86
87

AUTHORS

89       Sylvain  Conchon  <conchon@lri.fr>  and   Evelyne   Contejean   <conte‐
90       jea@lri.fr>
91
92
93

SEE ALSO

95       Alt-Ergo web site: http://alt-ergo.lri.fr
96
97
98
99                                 October, 2006                     Alt-Ergo(1)