Alt-Ergo(1)
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.
- -arrays
- Theory of functional arrays. In order to use this theory, you should add the following prelude in your files:
- type 'a farray
- logic get : 'a farray, int -> 'a
- logic set : 'a farray, int, 'a -> 'a farray
- -pairs Theory of pairs. In order to use this theory, you should add the
- following prelude in your files:
- 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>
SEE ALSO
- Alt-Ergo web site: http://alt-ergo.lri.fr