Previous Up Next

Appendix A  Release Notes

A.1  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.1 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.1: Syntax changes from version 0.73 to version 0.80

A.2  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