Commit e112153a authored by Guillaume Melquiond's avatar Guillaume Melquiond

New release.

parent ac9f96ec
:x: marks a potential source of incompatibility :x: marks a potential source of incompatibility
Version 1.0.0, June 25, 2018
----------------------------
Core Core
* improved support of counter-examples * improved support of counter-examples
* attribute `[@vc:sp]` on an expression switches from traditional WP
to Flanagan-Saxe-like VC generation
* type invariants now produce logical axioms;
a type with an invariant must be proved to be inhabited :x:
* logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any more,
so equality functions must be declared/defined on a per-type basis
(already done for type `int` in the standard library) :x:
Language Language
* numerous changes to syntax, see documentation appendix :x: * numerous changes to syntax, see documentation appendix :x:
* `let function`, `let predicate`, `val function`, and `val predicate` * `let function`, `let predicate`, `val function`, and `val predicate`
introduce symbols in both logic and programs introduce symbols in both logic and programs
* logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any more,
so equality functions must be declared/defined on a per-type basis
(already done for type `int` in the standard library) :x:
* added overloading of program symbols * added overloading of program symbols
* new contract clause `alias { <term> with <term>, ... }` :x: * new contract clause `alias { <term> with <term>, ... }` :x:
* support for parallel assignment `<term>,... <- <term>,...` * support for parallel assignment `<term>,... <- <term>,...`
* type invariants now produce logical axioms;
a type with an invariant must be proved to be inhabited :x:
* support for local exceptions using `exception ... in ...` * support for local exceptions using `exception ... in ...`
* added `break`, `continue`, and `return` statements * added `break`, `continue`, and `return` statements
* support for `exception` branches in `match` constructs * support for `exception` branches in `match` constructs
* support for `for` loops on range types * support for `for` loops on range types
(including machine integers from the standard library) (including machine integers from the standard library)
* attribute `[@vc:sp]` on an expression switches from traditional WP
to Flanagan-Saxe-like VC generation
* support for type coercions in logic using `meta coercion` * support for type coercions in logic using `meta coercion`
* keyword `theory` is deprecated; use `module` instead * keyword `theory` is deprecated; use `module` instead
* term on the left of sequence `;` must be of type `unit` :x: * term on the left of sequence `;` must be of type `unit` :x:
......
...@@ -112,7 +112,6 @@ ...@@ -112,7 +112,6 @@
============ Making a release ============ ============ Making a release ============
* check the BTS * check the BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK * check that nightly bench is OK
* check that "make xml-validate-local" is OK * check that "make xml-validate-local" is OK
(see below : copy the dtd on the web) (see below : copy the dtd on the web)
......
VERSION=1.00+git VERSION=1.0.0
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment