# alt-ergo - Online in the Cloud

This is the command alt-ergo that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

### PROGRAM:

#### NAME

Alt-Ergo - An automatic theorem prover dedicated to program verification

#### SYNOPSIS

alt-ergo [ options ] file

#### DESCRIPTION

Alt-Ergo is an automatic theorem prover. It takes as inputs an arbitrary 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 provides a built-in type
('a,'b) farray and a built-in syntax for manipulating 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 values 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][1]

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 *)

#### ENVIRONMENTVARIABLES

ERGOLIB
Alternative path for the Alt-Ergo library

#### AUTHORS

Sylvain Conchon <[email protected]> and Evelyne Contejean <[email protected]>

Use alt-ergo online using onworks.net services

Free Servers & Workstations