diff --git a/examples/in_progress/binomial_heap.mlw b/examples/in_progress/binomial_heap.mlw index aa39d30f4b42b1fafb410e724c2ec264f952529b..1d41078d770701295cdeeaf0100d1b33053d7588 100644 --- a/examples/in_progress/binomial_heap.mlw +++ b/examples/in_progress/binomial_heap.mlw @@ -19,6 +19,7 @@ module BinomialHeap type tree = { elem: elt; children: list tree; + rank: int; } (* [e] is no greater than the roots of the trees in [l] *) @@ -41,14 +42,14 @@ module BinomialHeap lemma heaps_reverse: forall h. heaps h -> heaps (reverse h) - function rank (t: tree) : int = - length t.children + (* function rank (t: tree) : int = *) + (* length t.children *) function link (t1 t2: tree) : tree = if le t1.elem t2.elem then - { t1 with children = Cons t2 t1.children } + { elem = t1.elem; rank = t1.rank + 1; children = Cons t2 t1.children } else - { t2 with children = Cons t1 t2.children } + { elem = t2.elem; rank = t2.rank + 1; children = Cons t1 t2.children } function occ (x: elt) (l: list tree) : int = match l with @@ -86,7 +87,8 @@ module BinomialHeap end predicate binomial_tree (t: tree) = - has_order (rank t) t.children + t.rank = length t.children && + has_order t.rank t.children (* a binomial heap is a list of trees *) type heap = list tree @@ -96,7 +98,7 @@ module BinomialHeap predicate inv (m: int) (h: heap) = match h with | Nil -> true - | Cons t r -> let k = rank t in m <= k && binomial_tree t && inv (k + 1) r + | Cons t r -> let k = t.rank in m <= k && binomial_tree t && inv (k + 1) r end lemma inv_reverse: @@ -166,7 +168,7 @@ module BinomialHeap ensures { occ x result = occ x h + 1 } ensures { forall e. e <> x -> occ e result = occ e h } = - add_tree { elem = x; children = Nil } h + add_tree { elem = x; rank = 0; children = Nil } h let rec merge (ghost k: int) (h1 h2: heap) requires { heaps h1 } diff --git a/examples/in_progress/binomial_heap/why3session.xml b/examples/in_progress/binomial_heap/why3session.xml index 6ec0e36e6709632a21163b872f105893a609e790..2cc028f0208d4cc9d00eee4c60b5d879b65051e9 100644 --- a/examples/in_progress/binomial_heap/why3session.xml +++ b/examples/in_progress/binomial_heap/why3session.xml @@ -6,28 +6,30 @@ - + - + - + - + - + - + - + + + @@ -50,16 +52,16 @@ - + - + - + @@ -78,60 +80,60 @@ - - + - + - + - + - + - + - + - + - + - + - + - + - + + @@ -163,6 +165,7 @@ + @@ -170,25 +173,26 @@ - + - + - + + - + - + @@ -197,19 +201,24 @@ - + - + + + + + - + + - + @@ -218,25 +227,22 @@ - + - + - - - - - + - + - + + @@ -245,7 +251,7 @@ - + @@ -256,15 +262,18 @@ + + + @@ -274,20 +283,20 @@ - + - + - + - + @@ -296,40 +305,44 @@ + - + - + - + - + + + - + - + - + + @@ -348,16 +361,16 @@ - + - + - + @@ -368,10 +381,10 @@ - + - + diff --git a/examples/in_progress/binomial_heap/why3shapes.gz b/examples/in_progress/binomial_heap/why3shapes.gz index 19dfc98cd31ed5dcb5c9d679192859ad1d0f9263..ff575f0cdbb962b4ac645b69d623822b264b58dd 100644 Binary files a/examples/in_progress/binomial_heap/why3shapes.gz and b/examples/in_progress/binomial_heap/why3shapes.gz differ