Previous Up Next

Appendix A  Release Notes

A.1  Release Notes for version 1.0: syntax changes w.r.t. 0.88

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 non-ghost code; in particular, there is no polymorphic equality in programs anymore, so equality functions must be declared/defined on a per-type basis (already done for type int in the standard library). The CHANGES.md file describes other potential sources of incompatibility.


version 0.88version 1.0
function f ...let function f ... if called in programs
’L:label L in
at x ’Lx at L
\x. efun x -> e
use HighOrdnothing, not needed anymore
HighOrd.pred tyty -> bool
type t model ...type t = abstract ...
abstract e ensures { Q }begin ensures { Q } e end
namespace Nscope N
use import Muse M
"attribute"[@attribute]
meta M prop Pmeta M lemma P or meta M axiom P or meta M goal P
loop ... endwhile true do ... done
type ... invariant { ... self.foo ... }type ... invariant { ... foo ... }
Figure A.1: Syntax changes from version 0.88 to version 1.0

Here are a few more semantic changes

Proving only partial correctness
In versions 0.xx of Why3, when a program function is recursive but not given a variant, or contains a while loop not given a variant, then it was assumed that the user wants to prove partial correctness only. A warning was issued, recommending to add an extra 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 fine-grain 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>
Semantics of the any construct
The any construct in Why3 0.xx was introducing an arbitrary value satisfying the associated post-condition. 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

A.2  Release Notes for version 0.80: syntax changes w.r.t. 0.73

The syntax of WhyML programs changed in release 0.80. The table in Figure A.2 summarizes the changes.


version 0.73version 0.80
type t = {| field : int |}type t = { field : int }
{| field = 5 |}{ field = 5 }
use import module Muse 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 }
    = e
val 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 }
Figure A.2: Syntax changes from version 0.73 to version 0.80

A.3  Summary of Changes w.r.t. Why 2

The main new features with respect to Why 2.xx are the following.

  1. Completely redesigned input syntax for logic declarations
  2. More generic handling of goals and lemmas to prove
  3. Source code organized as a library with a documented API, to allow access to Why3 features programmatically.
  4. GUI with new features with respect to the former GWhy
  5. Extensible architecture via plugins

Previous Up Next