Try-Alt-Ergo is a JavaScript-based version of Alt-Ergo that can be run on compatible browsers (eg. Firefox, Chromium) without requiring a server for computations.
Alt-Ergo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why platform. Currently, it is used as a back-end of different tools and in various settings, especially via the Why3 platform. For instance, the Frama-C suite relies on it to prove formulas generated from C code, and the SPARK toolset uses it to check formulas produced from Ada programs. In addition, Alt-Ergo is used to prove formulas issued from B modelizations and from cryptographic protocols verification.
Alt-Ergo's native input language is a polymorphic first-order logic "à la ML" modulo theories. This logic is very suitable for expressing formulas generated in the context of program verification. Currently, Alt-Ergo is capable of reasoning in the combination of the following built-in theories:
This page aims to output all the messages returned by Alt-Ergo. On this page, you will find more information than in the output console, such as debug informations (if set).
This section is still Work In Progress
At this time it only outputs the usage of axioms in instances
type 'a set
logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop
axiom mem_add:
forall x, y : 'a. forall s : 'a set.
mem(x, add(y, s)) <-> (x = y or mem(x, s))
logic is1, is2 : int set
logic iss : int set set
goal g:
is1 = is2 ->
mem (is1, add (is2, iss))
goal g_1 :
forall x,y,z,t:int.
0 <= y + z <= 1 ->
x + t + y + z = 1 ->
y + z <> 0 ->
x + t = 0
logic h,g,f: int,int -> int
logic a, b:int
goal g_2 :
h(g(a,a),g(b,b)) = g(b,b) ->
a = b ->
g(f(h(g(a,a),g(b,b)),b) - f(g(b,b),a),
f(h(g(a,a),g(b,b)),a) - f(g(b,b),b))
= g(0,0)
type 'a pointer
type 'a pset
logic P : int -> prop
logic Q : int , int -> prop
axiom a:
(forall x:int.
(P(x) <->
(exists i:int. exists r: int.
Q(r,i)
)
)
)
goal g_3 :
Q(1,2) -> P(4)
type 'a set
logic empty : 'a set
logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop
axiom mem_empty:
forall x : 'a.
not mem(x, empty : 'a set)
axiom mem_add:
forall x, y : 'a. forall s : 'a set.
mem(x, add(y, s)) <-> (x = y or mem(x, s))
logic is1, is2 : int set
logic iss : int set set
goal g_4:
is1 = is2 ->
(not mem(1, add(2+3, empty : int set))) and
mem (is1, add (is2, iss))
goal g_5 :
forall i,j,k:int.
forall v,w : 'a.
forall b : 'a farray.
b = b[j<-b[i],k<-w] ->
i = 1 ->
j = 2 ->
k = 1 ->
b[i] = b[j]
type t = A | B | C | D
type t2 = E | F | G | H
goal g_6 :
forall a : (t,t2) farray.
a[B <- E][A] <> E ->
a[C <- F][A] <> F ->
a[D <- G][A] <> G ->
a[A] = H
goal g_7 :
forall x,y,z:int.
x > 3 ->
y > 0 ->
z > 0 ->
y > z ->
z = ((x / y) + y) / 2 ->
z > 1 and y > 2
Try-Alt-Ergo is a work fully funded by OCamlPro, and maintained by the Alt-Ergo development team
This website uses the Alt-Ergo's web worker obtained by compiling the bytecode executable of the solver into JavaScript thanks to Js_of_ocaml. The web worker uses json file to receive input file as long as options and to send answers. This allows the web worker to be run directly in Js code such as in the Try-Alt-Ergo tutorial. We use the Data-encoding library to convert our data to json throught OCaml code. Alt-Ergo also needs Zarith stubs js to be compiled in Js.
Try-Alt-Ergo uses the Lwt library to run the Alt-Ergo web worker. It uses a combination of Tyxml, Bootstrap and the Ace code editor to produce the resulting website.