Homepage > Man Pages > Category > General Commands
Homepage > Man Pages > Name > A


man page of alt-ergo

alt-ergo: An automatic theorem prover dedicated to program verification


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


alt-ergo [ options ] files
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.
-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. -pairs Theory of pairs. In order to use this theory, you should add the following prelude in your files: type 'a pair logic pair : 'a, 'a -> 'a pair logic fst: 'a pair -> 'a logic snd: 'a pair -> 'a


ERGOLIB Alternative path for the Alt-Ergo library


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


Alt-Ergo web site: //alt-ergo.lri.fr October, 2006 ALT-ERGO(1)

Copyright © 2011–2018 by topics-of-interest.com . All rights reserved. Hosted by all-inkl.
Contact · Imprint · Privacy

Page generated in 25.40ms.

laufbaender.name | brauchbar.de | daelim-forum.spreadshirt.de