Linux Certif

Toute la documentation sur la certification Linux LPI

alt-ergo

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