Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Project Filelist for Why3

File Release Notes and Changelog

Release Name: 0.70

Release Notes
version 0.70, July 7, 2011

  New features

  o [WhyML] language and VC generator
  o [syntax] record types
    - introduced with syntax "type t = {| a:int; b:bool |}"
      actually syntactic sugar for "type t = `mk t' (a:int) (b:bool)"
      i.e. an algebraic with one constructor and projection functions
    - a record expression is written {| a = 1; b = True |}
    - access to field a with syntax x.a
    - update with syntax {| x with b = False |}
    - record patterns
  o new tool why3replayer: batch replay of a Why3 session created in IDE
  o [Alt-Ergo/Z3/CVC3/Yices output] support for built-in theory of arrays

  Fixes and other changes

  * [syntax] new syntax for conjunction (/\) and disjunction (\/)
    ("and" and "or" do not exist anymore)
  * [syntax] "logic" is not a keyword anymore, use "function" and "predicate"
  o [IDE] interactive detection of provers disabled because incompatible
    with session. Detection must be done with why3config --detect-provers
  o [IDE] bug 12244 resolved by using Task.task_equal
  o [IDE] tool "Replay" works
  o [IDE] tool "Reload" reloads the file from disk. No need to exit IDE anymore
  o [IDE] does not use Threads anymore, thanks to Call_provers.query_call
  o [IDE] displays explanations using labels of the form "expl:..."
  o [IDE] dropped dependence on Sqlite3
  o [Alt-Ergo output] bugfix: no triggers for "exists" quantifier
  o [Coq output] bugfix: polymorphic inductive predicates
  o [Coq output] fixed bug 12934: type def with several type params
  * [API] functions to create an environment are now exported from Env
  * [API] calls to prover can now be asynchronous
    Driver.prove_task now returns some intermediate value
    (of type prover_call), which can be queried in two ways:
    - blocking way with Call_provers.wait_on_call
    - non-blocking way with Call_provers.query_call
    So old code performing "prove_task t () ()" should be translated to
    "wait_on_call (prove_task t ()) ()".