[Caml-list] [ANN] InvarGenT v1.2: GADTs for invariants and postconditions

[Caml-list] [ANN] InvarGenT v1.2: GADTs for invariants and postconditions

[Lukasz Stafiniak]

[-- Attachment #1: Type: text/plain, Size: 1306 bytes --]

I am pleased to release version 1.2 of InvarGenT, a system that infers
invariants and postconditions, and exports the corresponding GADTs-based
OCaml code.
https://github.com/lukstafi/invargent/releases

The highlight of this release is the AVL trees example see:
https://github.com/lukstafi/invargent/blob/master/examples/avl_tree.gadt
https://github.com/lukstafi/invargent/blob/master/examples/avl_tree.gadti.target
InvarGenT finds out that the height of a rotated tree can be the same as
original tree or one bigger, the same fact for the tree with added element,
that the height of merger of two trees is at most one bigger than that of
the larger tree, and that removing an element can decrease the height of a
tree, by at most 1.

Changes:
* Several bug fixes.
* So-called "opti" relations: "k=min(m,n)" and "k=max(m,n)" in the
numerical sort.
* So-called "subopti" relations "k<=max(m,n)" and "min(m,n)<=k" in the
numerical sort.
* Less confusing syntax for existential types, "datatype" and "datacons"
keywords.
* Pattern-matching guards "when e1 <= e2", where e1 and "e2 are expressions
of type "Num".
* Positive assert clauses, "assert num e1 <= e2; ..." and "assert type e1 =
e2; ...".
* Flagship example: AVL trees with imbalance of 2 (based on the
implementation from OCaml standard library).

[-- Attachment #2: Type: text/html, Size: 4344 bytes --]