Commit 63d89abb authored by Andrei Paskevich's avatar Andrei Paskevich

make programs in the gallery compatible with whyml

parent ec869ddc
......@@ -98,6 +98,11 @@ module HashTableImpl
h.contents <- const None
{ valid h /\ forall k: 'a. get h k = None }
let idx (h: t 'a 'b) (k: 'a) =
{ }
mod (abs (hash k)) (length h.data)
{ result = idx h k }
let add (h: t 'a 'b) (k: 'a) (v: 'b) =
{ valid h }
let i = idx h k in
......
......@@ -77,6 +77,11 @@ module Iterator
predicate hasNext (i: iterator) = i.it <> Done
let hasNext (i: iterator) =
{ }
i.it <> Done
{ result = True <-> hasNext i }
let next (i: iterator) =
{ hasNext i }
match i.it with
......@@ -154,7 +159,7 @@ module ITree
bst_mem x t.tree
{ result=True <-> mem x t.tree }
let add (t: itree) (x: elt) =
let add (t: itree) (x: elt) =
{ inv t }
try t.tree <- bst_add x t.tree; True
with Already -> False
......
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