Commit 12379417 authored by Andrei Paskevich's avatar Andrei Paskevich

minor changes in examples

avoid using logical symbols in programs in a few places
parent 85074baf
module Bag
use BuiltIn
use import int.Int
type bag 'a = 'a -> int
......@@ -13,10 +12,10 @@ module Bag
fun _ -> 0
let ghost function add (e: 'a) (b: bag 'a): bag 'a =
fun x -> if BuiltIn.(=) x e then b x + 1 else b x
fun x -> if pure {x = e} then b x + 1 else b x
let ghost function remove (e: 'a) (b: bag 'a): bag 'a =
fun x -> if BuiltIn.(=) x e then b x - 1 else b x
fun x -> if pure {x = e} then b x - 1 else b x
end
......
......@@ -105,4 +105,4 @@ module DFS
assert { well_colored !marked !busy };
dfs root
end
\ No newline at end of file
end
......@@ -43,7 +43,6 @@ end
*)
module Utils_Spec
use BuiltIn
use import int.Int
use import int.NumOf
use import bv.BV32
......@@ -79,8 +78,7 @@ module Utils_Spec
variant {bv with ult}
ensures {t'int (count bv) = NumOf.numof (nth bv) 0 32}
=
if BuiltIn.(=) bv zeros then ()
else
if pure { bv <> zeros } then
begin
countSpec_Aux (lsr_bv bv one);
assert {
......@@ -92,7 +90,7 @@ module Utils_Spec
NumOf.numof f 0 32 - x = NumOf.numof f (0+1) 32 &&
NumOf.numof f (0+1) (31+1) = NumOf.numof h 0 31 &&
NumOf.numof g 0 (32-1) = NumOf.numof g 0 32
}
}
end
(** With these lemmas, we can now prove the correctness property of
......
......@@ -105,10 +105,11 @@ module Treedel
| Top
| Left (zipper 'a) 'a (tree 'a)
function zip (t: tree 'a) (z: zipper 'a) : tree 'a = match z with
let rec function zip (t: tree 'a) (z: zipper 'a) : tree 'a
= match z with
| Top -> t
| Left z x r -> zip (Node t x r) z
end
end
lemma inorder_zip:
forall z "induction": zipper 'a, x: 'a, l r: tree 'a.
......
......@@ -18,10 +18,11 @@ module Tree
type tree = Leaf | Node tree tree
(* the list of leaf depths for tree t, if root is at depth d *)
function depths (d: int) (t: tree) : list int = match t with
let rec function depths (d: int) (t: tree) : list int =
match t with
| Leaf -> Cons d Nil
| Node l r -> depths (d+1) l ++ depths (d+1) r
end
end
(* lemmas on depths *)
......
......@@ -11,7 +11,7 @@ theory Map
let function get (f: map 'a 'b) (x: 'a) : 'b = f x
let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
fun y -> if y = x then v else f y
fun y -> if pure {y = x} then v else f y
(** syntactic sugar *)
let function ([]) (f: map 'a 'b) (x: 'a) : 'b = f x
......
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