Migration from Why 2.xx to Why3

This document gives the essential changes to perform when migrating from Why2 to Why3.

Of course, this does not replace the Why3 manual.

Theories

In Why3, every declaration must be done inside a theory. Thus to migrate a Why2 file into a Why3 one, a first thing to do is to enclose the contents of the file as 
theory T

use import bool.Bool
use import int.Int
...

end
The first two imports correspond to the inclusion of the Why2 prelude. Generally speaking, the Why2 inclusion of other files does not exist anymore, and proper importation clauses must be used instead, e.g 
include "division.why"
must be replaced by 
use import int.Computer_division
This declaration imports the theory called Computer_division from the file int.why of the Why3 standard library.

Changes in the logic language

The following table provides a quick reference to syntax changes in the logic language
Why 2.xx Why3 0.7x and 0.8x
type 'a t type t 'a
logic f: int, bool -> int function f int bool : int
logic p: int, bool -> prop predicate p int bool
function f (x: int, y:bool) = e function f (x: int) (y:bool) = e
predicate p (x: int, y:bool) = e predicate p (x: int) (y:bool) = e
inductive p : int, bool -> prop = ... inductive p int bool = ...
f(t1,t2,t3) (f t1 t2 t3)
f1 and f2 f1 /\ f2
f1 or f2 f1 \/ f2
(label : f) "label" f
true (of type bool) True
false (of type bool) False
void ()
unit ()

Changes in ML programs

Beware that the syntax is slight different between version 0.7x and version 0.8x. Programs must be in .mlw files, and inside a module declaration of the form 
module M

use import bool.Bool
use import int.Int
use import ref.Ref
use import array.Array

...

end
Note that in Why3 0.73 or lower, importation of modules had the form 
use import module ref.Ref
use import module array.Array
Why 2.xx Why3 0.8x former Why3 0.7x
int ref ref int
{ ... x ... } { ... !x ... }
{ ... x@ ... } { ... (old !x) ... }
{ ... x@L ... } { ... (at !x 'L) ... }
L: e 'L : e
exception Exc of t exception Exc t
let f (x:int) (y:int) : t = { P } e { Q | Exc -> R } let f (x:int) (y:int) : t requires { P } ensures { Q } raises { Exc -> R} = e let f (x:int) (y:int) : t = { P } e { Q } | Exc -> { R }
parameter f: x:int -> y:int -> { P } t writes a,b { Q | Exc -> R } val f (x:int) (y:int) : t requires { P } writes { a,b } ensures { Q } raises { Exc -> R} val f (x:int) (y:int) : { P } t writes a b { Q } | Exc -> { R }
parameter f: int -> unit -> { P } t writes a,b { Q | Exc -> R } val f : int -> unit -> t requires { P } writes { a,b } ensures { Q } raise { Exc -> R } val f : int -> unit -> { P } t writes a b { Q } | Exc -> { R }
while c do { invariant f variant t} e done while c do invariant { f } variant { t } e done
while c do { invariant f variant t for R } e done while c do invariant { f } variant { t } with R e done
e {{ p }} abstract e ensures { p } abstract e { p }
Why3 0.83: abstract ensures { p } e end

Examples of Why3 programs are available in Toccata's gallery.

Why3 homepage