why(1) [debian man page]

why(1)							      General Commands Manual							    why(1)

NAME

       why - A multi-language multi-prover verification tool

SYNOPSIS

       why [ options ] files

DESCRIPTION

       why is a verification tool.  It takes annotated programs as input (in ML or C syntax) and outputs verification conditions for several proof
       assistants (Coq, PVS, HOL Light, Mizar) and decision procedures (haRVey, Simplify).

OPTIONS

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

AUTHORS

       Jean-Christophe Filliatre <filliatr@lri.fr>

SEE ALSO

       Why web site: http://why.lri.fr/

								    March, 2002 							    why(1)

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

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.

       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.

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)