From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 28E147EFCB for ; Tue, 18 Feb 2014 20:03:07 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lukstafi@gmail.com) identity=pra; client-ip=74.125.82.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lukstafi@gmail.com designates 74.125.82.172 as permitted sender) identity=mailfrom; client-ip=74.125.82.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f172.google.com) identity=helo; client-ip=74.125.82.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-we0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AicCAHGtA1NKfVKslGdsb2JhbABZgkJ8V78HT4EUCBYOAQEBAQcLCwkSKoJsARsWCAMSEF0BEQEFASIbh2gBAxENmyqDCoxegw6VPQoZJw1khysRAQEEDIJQjCGCOg+BegSYLJA2GCmEWjs X-IPAS-Result: AicCAHGtA1NKfVKslGdsb2JhbABZgkJ8V78HT4EUCBYOAQEBAQcLCwkSKoJsARsWCAMSEF0BEQEFASIbh2gBAxENmyqDCoxegw6VPQoZJw1khysRAQEEDIJQjCGCOg+BegSYLJA2GCmEWjs X-IronPort-AV: E=Sophos;i="4.97,502,1389740400"; d="scan'208";a="49559572" Received: from mail-we0-f172.google.com ([74.125.82.172]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 18 Feb 2014 20:03:06 +0100 Received: by mail-we0-f172.google.com with SMTP id u56so2090400wes.3 for ; Tue, 18 Feb 2014 11:03:06 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=mjoCsvXTBkFg0QPICLADqygXOH1ZBV6KGSnIWO/zONw=; b=y2z0pvoWKY2RgtAZXD+o5Y7eEqLmlrq6A2FSEHmcaDU1POIV03kSTLzzP/1SNA/QB+ sQU8zc6YqzUsEEFv/fxKEn2/tj5VrunU9vNh7LhTMuoKq029w60DfJHb0TpxZVt+16oQ aSwX4sS9zDqGd3cdx9qnZMN37s+gzPg5DEOU3AJMQm8bjGo1Kx2AxmFxqzoeRV5ki/qh RN8UfIP7cA9qZP+XX7q8QDMIMQ6LTVy+50c9kl+bmmKw/O195woQ2bFLCLDUcZ3Y+two uhmcWnoULdHdNSXTHorGO3JoaPADUGmvsTtNUuT0M0SDPuTMnQpe2QA++twKojfOqK3y 4V5w== X-Received: by 10.194.60.37 with SMTP id e5mr23794141wjr.32.1392750186130; Tue, 18 Feb 2014 11:03:06 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.49.71 with HTTP; Tue, 18 Feb 2014 11:02:45 -0800 (PST) From: Lukasz Stafiniak Date: Tue, 18 Feb 2014 20:02:45 +0100 Message-ID: To: Caml Content-Type: multipart/alternative; boundary=047d7ba979da1af34704f2b2ec39 Subject: [Caml-list] [ANN] InvarGenT v1.2: GADTs for invariants and postconditions --047d7ba979da1af34704f2b2ec39 Content-Type: text/plain; charset=ISO-8859-1 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). --047d7ba979da1af34704f2b2ec39 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
I am pleased to release versi= on 1.2 of InvarGenT, a system that infers invariants and postconditions, an= d exports the corresponding GADTs-based OCaml code.
https://github.com/lukstafi/invargent/releases

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

Changes:
* Several bug fixes.
* So-called "opti" relations: "k=3Dmin(m,n)" a= nd "k=3Dmax(m,n)" in the numerical sort.
* So-called "subopti" relations "k<= =3Dmax(m,n)" and "min(m,n)<=3Dk" in the numerical sort.
* Less confusing syntax for=A0existential types,=A0"datatype" and &qu= ot;datacons" keywords.
* Pattern-matching guards "when e1 <=3D e2&qu= ot;, where e1 and "e2 are expressions of type "Num".<= /font>
* Positive assert clauses, "assert num e1 <= =3D e2; ..." and "assert type e1 =3D e2; ...".=
* Flagship example: AVL trees with imbalance of 2 (based o= n the implementation from OCaml standard library).

--047d7ba979da1af34704f2b2ec39--