This document gives the essential changes to perform when migrating from Why2 to Why3.
Of course, this does not replace the Why3 manual.
theory T use import bool.Bool use import int.Int ... endThe 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_divisionThis declaration imports the theory called Computer_division from the file int.why of the Why3 standard library.
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 | () |
module M use import bool.Bool use import int.Int use import ref.Ref use import array.Array ... endNote 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.