Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
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][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 *)

ENVIRONMENT VARIABLES
       ERGOLIB
	      Alternative path for the Alt-Ergo	library

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

SEE ALSO
       Alt-Ergo	web site: http://alt-ergo.lri.fr

			       (C)  2006 -- 2013		   Alt-Ergo(1)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | EXAMPLES | ENVIRONMENT VARIABLES | AUTHORS | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=alt-ergo&sektion=1&manpath=FreeBSD+12.1-RELEASE+and+Ports>

home | help