Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit c709b941 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

snapshotable trees with additional comments

parent 9936d6ea
......@@ -7,6 +7,8 @@ Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and Peter Sestoft
VSTTE 2012
*)
(* Purely applicative binary trees with elements at the nodes *)
theory Tree
use export int.Int
......@@ -14,8 +16,6 @@ theory Tree
use export list.Length
use export list.Append
(* binary trees with elements at the nodes *)
type elt = int
type tree =
......@@ -34,12 +34,12 @@ theory Tree
end
(* Purely applicative iterators over binary trees *)
module Enum
use import Tree
(* the left spine of a tree, as a bottom-up list *)
type enum =
| Done
| Next elt tree enum
......@@ -49,8 +49,6 @@ module Enum
| Next x r e -> Cons x (tree_elements r ++ enum_elements e)
end
(* the enum of a tree [t], prepended to a given enum [e] *)
let rec enum t e variant { length (tree_elements t) } =
{ }
match t with
......@@ -61,6 +59,8 @@ module Enum
end
(* Mutable iterators with a Java-like API *)
module Iterator
use import Tree
......@@ -87,6 +87,8 @@ module Iterator
end
(* Binary search trees *)
module BSTree
use export Tree
......@@ -114,6 +116,7 @@ module BSTree
{ result=True <-> mem x t }
exception Already
(* bst_add raises exception Already when the element is already present *)
let rec bst_add (x: elt) (t: tree) =
{ bst t }
......@@ -130,6 +133,8 @@ module BSTree
end
(* Imperative trees with add/contains/snapshot/iterator API *)
module ITree
use export module BSTree
......@@ -189,7 +194,6 @@ module Harness
()
done
end
(*
......
......@@ -4,7 +4,7 @@
name="examples/programs/snapshotable_trees/why3session.xml">
<prover
id="0"
prover_id="alt-ergo" name="Alt-Ergo"
name="Alt-Ergo"
version="0.93.1"/>
<file
name="../snapshotable_trees.mlw"
......@@ -13,20 +13,20 @@
<theory
name="Tree"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="10" loccnumb="7" loccnume="11"
loclnum="12" loccnumb="7" loccnume="11"
verified="false"
expanded="false">
</theory>
<theory
name="WP Enum"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="37" loccnumb="7" loccnume="11"
loclnum="39" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
<goal
name="WP_parameter enum"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="54" loccnumb="10" loccnume="14"
loclnum="52" loccnumb="10" loccnume="14"
expl="parameter enum"
sum="19b39be8f7cad617d31f5b770677ced5"
proved="true"
......@@ -42,7 +42,7 @@
<goal
name="WP_parameter enum.1"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="54" loccnumb="10" loccnume="14"
loclnum="52" loccnumb="10" loccnume="14"
expl="parameter enum"
sum="b1459135c44cadc182ce5ae4b2ba4003"
proved="true"
......@@ -61,7 +61,7 @@
<goal
name="WP_parameter enum.2"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="54" loccnumb="10" loccnume="14"
loclnum="52" loccnumb="10" loccnume="14"
expl="parameter enum"
sum="71a69a5fdd27967b19cf6a7c53fbd7ec"
proved="true"
......@@ -80,7 +80,7 @@
<goal
name="WP_parameter enum.3"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="54" loccnumb="10" loccnume="14"
loclnum="52" loccnumb="10" loccnume="14"
expl="parameter enum"
sum="68dd5c82d4512ac2868d7c6303254537"
proved="true"
......@@ -147,13 +147,13 @@
<theory
name="WP BSTree"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="90" loccnumb="7" loccnume="13"
loclnum="92" loccnumb="7" loccnume="13"
verified="true"
expanded="false">
<goal
name="WP_parameter bst_mem"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="106" loccnumb="10" loccnume="17"
loclnum="108" loccnumb="10" loccnume="17"
expl="parameter bst_mem"
sum="98ef7877df601ae4f74051120b27f646"
proved="true"
......@@ -172,7 +172,7 @@
<goal
name="WP_parameter bst_add"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="118" loccnumb="10" loccnume="17"
loclnum="121" loccnumb="10" loccnume="17"
expl="parameter bst_add"
sum="e2d1eca5b2358e4f0187d4cee0318a02"
proved="true"
......@@ -192,13 +192,13 @@
<theory
name="WP ITree"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="133" loccnumb="7" loccnume="12"
loclnum="138" loccnumb="7" loccnume="12"
verified="true"
expanded="false">
<goal
name="WP_parameter create"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="142" loccnumb="6" loccnume="12"
loclnum="147" loccnumb="6" loccnume="12"
expl="normal postcondition"
sum="7e0b61d4119beffebe181a09add632a5"
proved="true"
......@@ -217,7 +217,7 @@
<goal
name="WP_parameter contains"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="147" loccnumb="6" loccnume="14"
loclnum="152" loccnumb="6" loccnume="14"
expl="parameter contains"
sum="8546f1cd94820214de4e16308a046d41"
proved="true"
......@@ -236,7 +236,7 @@
<goal
name="WP_parameter add"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="parameter add"
sum="d059286d396a843e7d48f4604e18d1ac"
proved="true"
......@@ -252,7 +252,7 @@
<goal
name="WP_parameter add.1"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="precondition"
sum="3f55e8ede5d84484509126ea93347d41"
proved="true"
......@@ -271,7 +271,7 @@
<goal
name="WP_parameter add.2"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="normal postcondition"
sum="cc37c93150866708e00c59b3e5d82345"
proved="true"
......@@ -287,7 +287,7 @@
<goal
name="WP_parameter add.2.1"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="parameter add"
sum="450b5b781b4820a7b62541336e227297"
proved="true"
......@@ -306,7 +306,7 @@
<goal
name="WP_parameter add.2.2"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="parameter add"
sum="e3c81061c0389534ed53297569aa83f8"
proved="true"
......@@ -325,7 +325,7 @@
<goal
name="WP_parameter add.2.3"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="parameter add"
sum="650d07ab01cd909d51642c23d4c67aab"
proved="true"
......@@ -344,7 +344,7 @@
<goal
name="WP_parameter add.2.4"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="parameter add"
sum="3a978c9475ef8069e57c060cac569f74"
proved="true"
......@@ -365,7 +365,7 @@
<goal
name="WP_parameter add.3"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="152" loccnumb="6" loccnume="9"
loclnum="157" loccnumb="6" loccnume="9"
expl="normal postcondition"
sum="8b0eee286993af1fa9e24bf674584698"
proved="true"
......@@ -386,7 +386,7 @@
<goal
name="WP_parameter snapshot"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="160" loccnumb="6" loccnume="14"
loclnum="165" loccnumb="6" loccnume="14"
expl="normal postcondition"
sum="f12d2bf982c6c3e7e0c4b939b0b2b6e3"
proved="true"
......@@ -405,7 +405,7 @@
<goal
name="WP_parameter iterator"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="165" loccnumb="6" loccnume="14"
loclnum="170" loccnumb="6" loccnume="14"
expl="normal postcondition"
sum="e854dbe1b8764b30827bc8997df577c9"
proved="true"
......@@ -425,13 +425,13 @@
<theory
name="WP Harness"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="172" loccnumb="7" loccnume="14"
loclnum="177" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
<goal
name="WP_parameter test"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="parameter test"
sum="9a9bf3c8e85e5aad109d3060c060132f"
proved="true"
......@@ -447,7 +447,7 @@
<goal
name="WP_parameter test.1"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="precondition"
sum="a3e7dc481a12db447f2b2af9db1ec8f2"
proved="true"
......@@ -466,7 +466,7 @@
<goal
name="WP_parameter test.2"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="precondition"
sum="8904bea4c86eedccaa8a78e8c1fc8095"
proved="true"
......@@ -485,7 +485,7 @@
<goal
name="WP_parameter test.3"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="precondition"
sum="55519355bf0e14cddd8e9b8bbd9c2825"
proved="true"
......@@ -504,7 +504,7 @@
<goal
name="WP_parameter test.4"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="assertion"
sum="845e4cb486e59257c20ba49be73e22e5"
proved="true"
......@@ -523,7 +523,7 @@
<goal
name="WP_parameter test.5"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="precondition"
sum="fc0418943d0b162553387f9ac6e23e36"
proved="true"
......@@ -542,7 +542,7 @@
<goal
name="WP_parameter test.6"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="precondition"
sum="cadbf5e00126da303e1032eddfcb1e3f"
proved="true"
......@@ -561,7 +561,7 @@
<goal
name="WP_parameter test.7"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="loop invariant init"
sum="8c450ca59d4bec2d6a97760a77b04517"
proved="true"
......@@ -580,7 +580,7 @@
<goal
name="WP_parameter test.8"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="precondition"
sum="5ce311a16179d9ac79972a53fd7f9038"
proved="true"
......@@ -599,7 +599,7 @@
<goal
name="WP_parameter test.9"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="precondition"
sum="872edec82e63d48d6a8af3d077a81b93"
proved="true"
......@@ -618,7 +618,7 @@
<goal
name="WP_parameter test.10"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="loop invariant preservation"
sum="a0f65c6230cc05ea72fcb4b906b806cd"
proved="true"
......@@ -637,7 +637,7 @@
<goal
name="WP_parameter test.11"
locfile="examples/programs/snapshotable_trees/../snapshotable_trees.mlw"
loclnum="176" loccnumb="6" loccnume="10"
loclnum="181" loccnumb="6" loccnume="10"
expl="loop variant decreases"
sum="f499cbdec47cda27da3e9ffaa88196f2"
proved="true"
......
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