alt-ergo(1)

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 ] file
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 a why
19       like syntax.
20
21

OPTIONS

23       -h     Help. Will give you the full list of command line options.
24
25

EXAMPLES

27       A theory of functional arrays with integer indexes . This  theory  pro‐
28       vides  a built-in type ('a,'b) farray and a built-in syntax for manipu‐
29       lating arrays.
30
31              For instance, given an abstract datatype tau  and  a  functional
32              array t of type (int, tau) farray declared as follows:
33
34              type tau
35
36              logic t : (int, tau) farray
37
38              The expressions:
39
40              t[i] denotes the value stored in t at index i
41
42              t[i1<-v1,...,in<-vn] denotes an array which stores the same val‐
43              ues as t for every index except  possibly  i1,...,in,  where  it
44              stores   value  v1,...,vn.  This  expression  is  equivalent  to
45              ((t[i1<-v1])[i2<-v2])...[in<-vn].
46
47
48              Examples.
49
50              t[0<-v][1<-w]
51
52              t[0<-v, 1<-w]
53
54              t[0<-v, 1<-w][1]
55
56
57
58       A theory of enumeration types.
59
60              For instance an enumeration type t with constructors A, B, C  is
61              defined as follows :
62
63              type t = A | B | C
64
65              Which  means  that all values of type t are equal to either A, B
66              or C. And that all these constructors are distinct.
67
68
69
70       A theory of polymorphic records.
71
72              For instance a polymorphic record type 'a t with  two  labels  a
73              and b of type 'a and int respectively is defined as follows:
74
75              type 'a t = { a : 'a; b : int }
76
77              The  expressions  {  a  =  4; b = 5 } and { r with b = 3} denote
78              records, while the dot notation r.a is used to access to labels.
79
80
81
82       Alt-Ergo (v. >= 0.95) allows the user to force the type of terms  using
83       the  syntax  <term>  : <type>. The example below illustrates the use of
84       this new feature.
85
86              type 'a list
87
88              logic nil : 'b list
89
90              logic f : 'c list -> int
91
92              goal g1 : f(nil) = f(nil) (* not valid because the two instances
93              of nil may have different types *)
94
95              goal g2 : f(nil:'d list) = f(nil:'d list) (* valid *)
96
97
98

ENVIRONMENT VARIABLES

100       ERGOLIB
101              Alternative path for the Alt-Ergo library
102
103
104

AUTHORS

106       Sylvain   Conchon   <conchon@lri.fr>   and  Evelyne  Contejean  <conte‐
107       jea@lri.fr>
108
109
110