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
    Eclipse Checkstyle Plug-in
    Eclipse Checkstyle Plug-in
    The Eclipse Checkstyle plug-in
    integrates the Checkstyle Java code
    auditor into the Eclipse IDE. The
    plug-in provides real-time feedback to
    the user about viol...
    Download Eclipse Checkstyle Plug-in
  • 2
    AstrOrzPlayer
    AstrOrzPlayer
    AstrOrz Player is a free media player
    software, part based on WMP and VLC. The
    player is in a minimalist style, with
    more than ten theme colors, and can also
    b...
    Download AstrOrzPlayer
  • 3
    movistartv
    movistartv
    Kodi Movistar+ TV es un ADDON para XBMC/
    Kodi que permite disponer de un
    decodificador de los servicios IPTV de
    Movistar integrado en uno de los
    mediacenters ma...
    Download movistartv
  • 4
    Code::Blocks
    Code::Blocks
    Code::Blocks is a free, open-source,
    cross-platform C, C++ and Fortran IDE
    built to meet the most demanding needs
    of its users. It is designed to be very
    extens...
    Download Code::Blocks
  • 5
    Amidst
    Amidst
    Amidst or Advanced Minecraft Interface
    and Data/Structure Tracking is a tool to
    display an overview of a Minecraft
    world, without actually creating it. It
    can ...
    Download Amidst
  • 6
    MSYS2
    MSYS2
    MSYS2 is a collection of tools and
    libraries providing you with an
    easy-to-use environment for building,
    installing and running native Windows
    software. It con...
    Download MSYS2
  • More »

Linux commands

  • 1
    a56
    a56
    A56 - Motorola DSP56001 assembler ...
    Run a56
  • 2
    a68g
    a68g
    a68g - Algol 68 Genie, an Algol 68
    compiler-interpreter ...
    Run a68g
  • 3
    copt
    copt
    copt - peephole optimizer SYSNOPIS:
    copt file.. DESCRIPTION: copt is a
    general-purpose peephole optimizer. It
    reads code from its standard input and
    writes an ...
    Run copt
  • 4
    copydatabase-1.3
    copydatabase-1.3
    copydatabase - Perform a
    document-by-document copy of one or more
    Xapian databases ...
    Run copydatabase-1.3
  • 5
    fweelin
    fweelin
    freewheeling � live looping musical
    instrument ...
    Run fweelin
  • 6
    fwexec
    fwexec
    fwexec - program to upload and rexecute
    image file to a connected NXT device ...
    Run fwexec
  • More »

Ad