GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages
Alt-Ergo(1) FreeBSD General Commands Manual Alt-Ergo(1)

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

alt-ergo [ options ] file

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.

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

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

ERGOLIB
Alternative path for the Alt-Ergo library

Sylvain Conchon <conchon@lri.fr> and Evelyne Contejean <contejea@lri.fr>

Alt-Ergo web site: http://alt-ergo.lri.fr
(C) 2006 -- 2013

Search for    or go to Top of page |  Section 1 |  Main Index

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with ManDoc.