Commit 6fba10e0 authored by Andrei Paskevich's avatar Andrei Paskevich

examples: make schorr_waite typecheck

Lsymbols in programs are probably more trouble than they are worth.
It took me ten minutes to find out why the whole program was ghost.
parent 3be1a2a5
......@@ -38,7 +38,7 @@ module SchorrWaite
(** the type of pointers and the null pointer *)
type loc
constant null: loc
val constant null: loc
val (=) (a b: loc) : bool
ensures { result = (a = b) }
......@@ -50,6 +50,9 @@ module SchorrWaite
val left: ref (map loc loc)
val right: ref (map loc loc)
(* FIXME: should we export this from map.Map? *)
let ([]) (m: map 'a 'b) (x: 'a) : 'b = m x
val get_left (p: loc) : loc
requires { p <> null }
ensures { result = !left[p] }
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