Man Linux: Main Page and Category List

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

                                 October, 2006                     Alt-Ergo(1)