EnglishFrenchSpanish

OnWorks favicon

alt-ergo - Online in the Cloud

Run alt-ergo in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

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

ENVIRONMENT VARIABLES


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

Download Windows & Linux apps

  • 1
    Free Pascal Compiler
    Free Pascal Compiler
    A 32/64/16-bit Pascal compiler for
    Win32/64/CE, Linux, Mac OS X/iOS,
    Android, FreeBSD, OS/2, Game Boy
    Advance, Nintendo NDS and DOS;
    semantically compatible wi...
    Download Free Pascal Compiler
  • 2
    Canon EOS DIGITAL Info
    Canon EOS DIGITAL Info
    Canon doesn�t have shutter count
    included on the EXIF information of an
    image file, as opposed to Nikon and
    Pentax. There�s no official Canon based
    application ...
    Download Canon EOS DIGITAL Info
  • 3
    rEFInd
    rEFInd
    rEFInd is a fork of the rEFIt boot
    manager. Like rEFIt, rEFInd can
    auto-detect your installed EFI boot
    loaders and it presents a pretty GUI
    menu of boot option...
    Download rEFInd
  • 4
    ExpressLuke GSI
    ExpressLuke GSI
    This SourceForge download page was to
    grant users to download my source built
    GSIs, based upon phhusson's great
    work. I build both Android Pie and
    Android 1...
    Download ExpressLuke GSI
  • 5
    Music Caster
    Music Caster
    Music Caster is a tray music player
    that lets you cast your local music to a
    Google Cast device. On the first run,
    you will need to click the arrow in your
    tas...
    Download Music Caster
  • 6
    PyQt
    PyQt
    PyQt is the Python bindings for
    Digia's Qt cross-platform
    application development framework. It
    supports Python v2 and v3 and Qt v4 and
    Qt v5. PyQt is avail...
    Download PyQt
  • More »

Linux commands

  • 1
    4ti2-circuits
    4ti2-circuits
    4ti2 - software package for algebraic,
    geometric and combinatorial problems on
    linear spaces ...
    Run 4ti2-circuits
  • 2
    4ti2-genmodel
    4ti2-genmodel
    4ti2 - software package for algebraic,
    geometric and combinatorial problems on
    linear spaces ...
    Run 4ti2-genmodel
  • 3
    coriander
    coriander
    coriander - control and display dc1394
    camera images ...
    Run coriander
  • 4
    corkscrew
    corkscrew
    corkscrew - Tunnel TCP connections
    through HTTP proxies ...
    Run corkscrew
  • 5
    g.gisenvgrass
    g.gisenvgrass
    g.gisenv - Outputs and modifies the
    user�s current GRASS variable settings.
    Prints all defined GRASS variables if no
    option is given. KEYWORDS: general,
    settin...
    Run g.gisenvgrass
  • 6
    g.guigrass
    g.guigrass
    g.gui - Launches a GRASS graphical user
    interface (GUI) session. Optionally
    updates default user interface settings.
    KEYWORDS: general, GUI, user interface ...
    Run g.guigrass
  • More »

Ad