Version 1.2 introduces a simplified syntax for reference variables, to avoid the somehow heavy OCaml syntax using bang character. In short, this is syntactic sugar summarized in the following table. An example using this new syntax is in examples/isqrt.mlw
autodereference syntax  desugared to 
let &x = ... in  let (x: ref ...) = ... in 
f x;  f x.contents; 
x < ...  x.contents < ... 
let ref x = ...  let &x = ref ... 
Notice that:
&
marker adds the typing constraint (x: ref ...)
let/val ref
and let/val &
are allowed
That syntactic sugar is further extended to pattern matching, function parameters and reference passing as follows.
autodereference syntax  desugared to  
match e with (x,&y) > y end  match e with (x,(y: ref ...)) > y.contents end  

 
let incr (ref x: int) ...  let incr (&x: ref int) ... 
The type annotation is not required. Letfunctions with such formal parameters also prevent the actual argument from autodereferencing when used in logic. Pure logical symbols cannot be declared with such parameters.
Autodereference suppression does not work in the middle of a relation
chain: in 0 < x :< 17
, x
will be dereferenced even if (:<)
expects a
refparameter on the left.
Finally, that syntactic sugar applies to the caller side:
autodereference syntax  desugared to  


The &
marker can only be attached to a variable. Works in logic.
Refbinders and &
binders in variable declarations, patterns,
and function parameters do not require importing ref.Ref
.
Any example that does not use references inside data structures
can be rewritten by using refbinders, without importing ref.Ref
.
Explicit use of type symbol "ref", program function "ref",
or field "contents" require importing ref.Ref
or why3.Ref.Ref
.
Operations (:=)
and (!)
require importing ref.Ref
.
Operation (:=)
is fully subsumed by direct assignment (<)
.
The syntax of WhyML programs changed in release 1.0. The table in Figure A.1 summarizes the changes.
Note also that logical symbols can no longer be used in nonghost code; in particular, there is no polymorphic equality in programs anymore, so equality functions must be declared/defined on a pertype basis (already done for type int in the standard library). The CHANGES.md file describes other potential sources of incompatibility.
version 0.88 version 1.0 function f ... let function f ... if called in programs ’L: label L in at x ’L x at L \x. e fun x > e use HighOrd nothing, not needed anymore HighOrd.pred ty ty > bool type t model ... type t = abstract ... abstract e ensures { Q } begin ensures { Q } e end namespace N scope N use import M use M "attribute" [@attribute] meta M prop P meta M lemma P or meta M axiom P or meta M goal P loop ... end while true do ... done type ... invariant { ... self.foo ... } type ... invariant { ... foo ... }
Here are a few more semantic changes
diverges
clause to that
function’s contract. It was also possible to disable that warning by
adding the label "W:diverges:N"
to the function’s
name. Version 1.00 of Why3 is more aggressively requiring the user
to prove the termination of functions which are not given the
diverges
clause, and the previous warning is now an
error. The possibility of proving only partial correctness is now
given on a more finegrain basis: any expression for which one wants
to prove partial correctness only, must by annotated with the
attribute [@vc:divergent]
.In other words, if one was using the following structure in Why3 0.xx:
let f "W:diverges:N" <parameters> <contract> = <body> 
then in 1.00 it should be written as
let f <parameters> <contract> = [@vc:divergent] <body> 
any
construct
in Why3 0.xx was introducing an arbitrary value satisfying the
associated postcondition. In some sense, this construct was
introducing some form of an axiom stating that such a value
exists. In Why3 1.00, it is now mandatory to prove the existence of
such a value, and a VC is generated for that purpose.To obtain the effect of the former semantics of the any
construct, one should use instead a local val
function. In other words, if one was using the following structure in Why3 0.xx:
any t ensures { P } 
then in 1.00 it should be written as
val x:t ensures { P } in x 
The syntax of WhyML programs changed in release 0.80. The table in Figure A.2 summarizes the changes.
version 0.73 version 0.80 type t = { field : int } type t = { field : int } { field = 5 } { field = 5 } use import module M use import M let rec f (x:int) (y:int) : t
variant { t } with rel =
{ P }
e
{ Q }
 Exc1 > { R1 }
 Exc2 n > { R2 }let rec f (x:int) (y:int) : t
variant { t with rel }
requires { P }
ensures { Q }
raises { Exc1 > R1
 Exc2 n > R2 }
= eval f (x:int) (y:int) :
{ P }
t
writes a b
{ Q }
 Exc1 > { R1 }
 Exc2 n > { R2 }val f (x:int) (y:int) : t
requires { P }
writes { a, b }
ensures { Q }
raises { Exc1 > R1
 Exc2 n > R2 }val f : x:int > y:int >
{ P }
t
writes a b
{ Q }
 Exc1 > { R1 }
 Exc2 n > { R2 }val f (x y:int) : t
requires { P }
writes { a, b }
ensures { Q }
raises { Exc1 > R1
 Exc2 n > R2 }abstract e { Q } abstract e ensures { Q }
The main new features with respect to Why 2.xx are the following.