# FreeBSD Manual Pages

```Alt-Ergo(1)		    General Commands Manual		   Alt-Ergo(1)

NAME
Alt-Ergo	 -  An automatic theorem prover	dedicated to program verifica-
tion

SYNOPSIS
alt-ergo	[ options ] file

DESCRIPTION
Alt-Ergo	is an automatic	theorem	prover.	 It takes as inputs  an	 arbi-
trary polymorphic and multi-sorted first-order formula written is a why
like syntax.

OPTIONS
-h     Help. Will give you the full list	of command line	options.

EXAMPLES
A theory	of functional arrays with integer indexes . This  theory  pro-
vides  a	built-in type ('a,'b) farray and a built-in syntax for manipu-
lating arrays.

For instance, given an abstract datatype tau  and	 a  functional
array t of type (int, tau) farray	declared as follows:

type tau

logic t :	(int, tau) farray

The expressions:

t[i] denotes the value stored in t at index i

t[i1<-v1,...,in<-vn] denotes an array which stores the same val-
ues as t for every index except  possibly	 i1,...,in,  where  it
stores   value  v1,...,vn.  This	expression  is	equivalent  to
((t[i1<-v1])[i2<-v2])...[in<-vn].

Examples.

t[0<-v][1<-w]

t[0<-v, 1<-w]

t[0<-v, 1<-w]

A theory	of enumeration types.

For instance an enumeration type t with constructors A, B, C  is
defined as follows :

type t = A | B | C

Which  means  that all values of type t are equal	to either A, B
or C. And	that all these constructors are	distinct.

A theory	of polymorphic records.

For instance a polymorphic record	type 'a	t with	two  labels  a
and b of type 'a and int respectively is defined as follows:

type 'a t	= { a :	'a; b :	int }

The  expressions	{  a  =	 4; b =	5 } and	{ r with b = 3}	denote
records, while the dot notation r.a is used to access to labels.

Alt-Ergo	(v. >= 0.95) allows the	user to	force the type of terms	 using
the  syntax  <term>  : <type>. The example below	illustrates the	use of
this new	feature.

type 'a list

logic nil	: 'b list

logic f :	'c list	-> int

goal g1 :	f(nil) = f(nil)	(* not valid because the two instances
of nil may have different	types *)

goal g2 :	f(nil:'d list) = f(nil:'d list)	(* valid *)

ENVIRONMENT VARIABLES
ERGOLIB
Alternative path for the Alt-Ergo	library

AUTHORS
Sylvain	 Conchon   _conchon@lri.fr_   and  Evelyne  Contejean  _conte-
jea@lri.fr_