Commit adf731d8 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix some syntax errors in examples.

parent 57d1a4be
...@@ -13,8 +13,8 @@ module BigNum ...@@ -13,8 +13,8 @@ module BigNum
use import int.Int use import int.Int
use import list.List use import list.List
constant base: int val constant base: int
axiom base_gt1: base > 1 ensures { result > 1 }
type digit = int type digit = int
type num = list digit type num = list digit
......
...@@ -19,7 +19,7 @@ module BinomialHeap ...@@ -19,7 +19,7 @@ module BinomialHeap
type elt type elt
predicate le elt elt val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le clone relations.TotalPreOrder with type t = elt, predicate rel = le
(** Trees. (** Trees.
...@@ -168,8 +168,7 @@ module BinomialHeap ...@@ -168,8 +168,7 @@ module BinomialHeap
let is_empty (h: heap) : bool let is_empty (h: heap) : bool
ensures { result <-> h = Nil } ensures { result <-> h = Nil }
= = match h with Nil -> true | _ -> false end
h = Nil
let get_min (h: heap) : elt let get_min (h: heap) : elt
requires { heaps h } requires { heaps h }
...@@ -193,7 +192,7 @@ module BinomialHeap ...@@ -193,7 +192,7 @@ module BinomialHeap
aux t.elem l aux t.elem l
end end
function link (t1 t2: tree) : tree = let function link (t1 t2: tree) : tree =
if le t1.elem t2.elem then if le t1.elem t2.elem then
{ elem = t1.elem; rank = t1.rank + 1; children = Cons t2 t1.children } { elem = t1.elem; rank = t1.rank + 1; children = Cons t2 t1.children }
else else
......
...@@ -54,7 +54,13 @@ module CoincidenceCountAnyType ...@@ -54,7 +54,13 @@ module CoincidenceCountAnyType
use list.Mem as L use list.Mem as L
use import int.Int use import int.Int
clone import relations.TotalStrictOrder type t
val predicate eq (x y : t)
ensures { result <-> x = y }
val predicate rel (x y : t)
clone import relations.TotalStrictOrder with type t, predicate rel
clone export list.Sorted clone export list.Sorted
with type t = t, predicate le = rel, goal Transitive.Trans with type t = t, predicate le = rel, goal Transitive.Trans
...@@ -67,7 +73,7 @@ module CoincidenceCountAnyType ...@@ -67,7 +73,7 @@ module CoincidenceCountAnyType
= =
match a, b with match a, b with
| Cons ha ta, Cons hb tb -> | Cons ha ta, Cons hb tb ->
if ha = hb then if eq ha hb then
add ha (coincidence_count ta tb) add ha (coincidence_count ta tb)
else if rel ha hb then else if rel ha hb then
coincidence_count ta b coincidence_count ta b
......
...@@ -33,7 +33,7 @@ module Esterel ...@@ -33,7 +33,7 @@ module Esterel
ghost mdl: set int; (* its interpretation as a set *) ghost mdl: set int; (* its interpretation as a set *)
} }
invariant { invariant {
forall i: int. (0 <= i < size /\ nth self.bv i) <-> mem i self.mdl forall i: int. (0 <= i < size /\ nth bv i) <-> mem i mdl
} }
......
...@@ -441,42 +441,47 @@ module KodaRuskey ...@@ -441,42 +441,47 @@ module KodaRuskey
assert { not (mem_stack i st') }; assert { not (mem_stack i st') };
let ghost visited1 = !visited in let ghost visited1 = !visited in
if bits[i] = White then begin if bits[i] = White then begin
'A: enum bits f0 (Cons f2 st'); label A in
enum bits f0 (Cons f2 st');
assert { sub st f0 bits.elts }; assert { sub st f0 bits.elts };
let ghost bits1 = map_of_array bits in let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in let ghost visited2 = !visited in
'B: bits[i] <- Black; label B in
bits[i] <- Black;
assert { sub st f0 bits.elts }; assert { sub st f0 bits.elts };
assert { white_forest f1 bits.elts }; assert { white_forest f1 bits.elts };
assert { unchanged (Cons f2 st') (at bits 'B).elts bits.elts}; assert { unchanged (Cons f2 st') (bits at B).elts bits.elts};
assert { inverse (Cons f2 st') (at bits 'A).elts bits.elts }; assert { inverse (Cons f2 st') (bits at A).elts bits.elts };
'C: enum bits f0 (Cons f1 (Cons f2 st')); label C in
enum bits f0 (Cons f1 (Cons f2 st'));
assert { bits[i] = Black }; assert { bits[i] = Black };
assert { final_forest f1 bits.elts }; assert { final_forest f1 bits.elts };
assert { if not (even_forest f1) assert { if not (even_forest f1)
then inverse (Cons f2 st') (at bits 'C).elts bits.elts && then inverse (Cons f2 st') (bits at C).elts bits.elts &&
white_forest f2 bits.elts white_forest f2 bits.elts
else unchanged (Cons f2 st') (at bits 'C).elts bits.elts && else unchanged (Cons f2 st') (bits at C).elts bits.elts &&
final_forest f2 bits.elts }; final_forest f2 bits.elts };
ghost stored_trans1 f0 bits1 (map_of_array bits) ghost stored_trans1 f0 bits1 (map_of_array bits)
i f1 f2 st' visited1 visited2 !visited i f1 f2 st' visited1 visited2 !visited
end else begin end else begin
assert { if not (even_forest f1) then white_forest f2 bits.elts assert { if not (even_forest f1) then white_forest f2 bits.elts
else final_forest f2 bits.elts }; else final_forest f2 bits.elts };
'A: enum bits f0 (Cons f1 (Cons f2 st')); label A in
enum bits f0 (Cons f1 (Cons f2 st'));
assert { sub st f0 bits.elts }; assert { sub st f0 bits.elts };
let ghost bits1 = map_of_array bits in let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in let ghost visited2 = !visited in
'B: bits[i] <- White; label B in
bits[i] <- White;
assert { unchanged (Cons f1 (Cons f2 st')) assert { unchanged (Cons f1 (Cons f2 st'))
(at bits 'B).elts bits.elts }; (bits at B).elts bits.elts };
assert { inverse (Cons f1 (Cons f2 st')) assert { inverse (Cons f1 (Cons f2 st'))
(at bits 'A).elts bits.elts }; (bits at A).elts bits.elts };
assert { sub st f0 bits.elts }; assert { sub st f0 bits.elts };
assert { if even_forest f1 || even_forest f2 assert { if even_forest f1 || even_forest f2
then unchanged st' (at bits 'A).elts bits.elts then unchanged st' (bits at A).elts bits.elts
else inverse st' (at bits 'A).elts bits.elts }; else inverse st' (bits at A).elts bits.elts };
'C: enum bits f0 (Cons f2 st'); enum bits f0 (Cons f2 st');
assert { bits[i] = White }; assert { bits[i] = White };
assert { white_forest f bits.elts }; assert { white_forest f bits.elts };
ghost stored_trans2 f0 bits1 (map_of_array bits) ghost stored_trans2 f0 bits1 (map_of_array bits)
......
...@@ -32,12 +32,12 @@ module FastExponentiation ...@@ -32,12 +32,12 @@ module FastExponentiation
while !e > 0 do while !e > 0 do
invariant { 0 <= !e /\ !r * power !p !e = power x n } invariant { 0 <= !e /\ !r * power !p !e = power x n }
variant { !e } variant { !e }
'L: label L in
if mod !e 2 = 1 then r := !r * !p; if mod !e 2 = 1 then r := !r * !p;
p := !p * !p; p := !p * !p;
e := div !e 2; e := div !e 2;
assert { power !p !e = assert { power !p !e =
let x = power (at !p 'L) !e in x * x } let x = power (!p at L) !e in x * x }
done; done;
!r !r
......
...@@ -42,7 +42,7 @@ module Memory ...@@ -42,7 +42,7 @@ module Memory
(** Memory blocks have two parts: a marking part containing in particular (** Memory blocks have two parts: a marking part containing in particular
Schorr-Waite internal management data, and a sequence of pointers Schorr-Waite internal management data, and a sequence of pointers
to other memory blocks. *) to other memory blocks. *)
type memory model { type memory = abstract {
(** Associate block size to location. *) (** Associate block size to location. *)
block_size : map loc int; block_size : map loc int;
(** Pointers to other memory blocks. *) (** Pointers to other memory blocks. *)
......
...@@ -64,11 +64,12 @@ module Memory ...@@ -64,11 +64,12 @@ module Memory
use import map.Map use import map.Map
(** [loc] is the type of memory locations (e.g pointers) *) (** [loc] is the type of memory locations (e.g pointers) *)
type loc type loc
val predicate eq (x y:loc) ensures { result <-> x = y }
(** Kinds of pointer fields. *) (** Kinds of pointer fields. *)
type kind = Parent | Left | Right type kind = Parent | Left | Right
(** Convenience alias for a pointer field table. *) (** Convenience alias for a pointer field table. *)
type pmem = map kind (map loc loc) type pmem = map kind (map loc loc)
type memory model { type memory = abstract {
mutable accessor : pmem; mutable accessor : pmem;
mutable mark : map loc bool; mutable mark : map loc bool;
} }
...@@ -109,7 +110,7 @@ module Memory ...@@ -109,7 +110,7 @@ module Memory
(** Non-deterministic initialization. In the original alorithm, (** Non-deterministic initialization. In the original alorithm,
the variable y starts uninitialized. *) the variable y starts uninitialized. *)
type non_det_magic type non_det_magic
type non_det model { mutable non_det_field : non_det_magic } type non_det = abstract { mutable non_det_field : non_det_magic }
val non_det : non_det val non_det : non_det
val anyloc () : loc writes { non_det } val anyloc () : loc writes { non_det }
...@@ -214,7 +215,7 @@ module TreeShape ...@@ -214,7 +215,7 @@ module TreeShape
= match t with = match t with
| Empty -> () | Empty -> ()
| Node l _ r -> | Node l _ r ->
if c2 = c then (unicity memo t t0 c p2 p;absurd); if eq c2 c then (unicity memo t t0 c p2 p;absurd);
aux l (memo[Left][c2]) c2; aux r (memo[Right][c2]) c2 aux l (memo[Left][c2]) c2; aux r (memo[Right][c2]) c2
end in end in
aux lf (memo[Left][c]) c; aux rg (memo[Right][c]) c aux lf (memo[Left][c]) c; aux rg (memo[Right][c]) c
...@@ -374,13 +375,13 @@ module Recursive ...@@ -374,13 +375,13 @@ module Recursive
let ghost _c = !x in let ghost _c = !x in
let _lf = get_acc Left !x in let _lf = get_acc Left !x in
let _rg = get_acc Right !x in let _rg = get_acc Right !x in
let ghost (lf, rg) = match t with let (lf, rg) = ghost match t with
| Empty -> absurd | Empty -> absurd
| Node l _ r -> (l, r) | Node l _ r -> (l, r)
end in end in
(ghost not_below mem0 lf rg _c !z); (ghost not_below mem0 lf rg _c !z);
bloc mem0 GoLeft; bloc mem0 GoLeft;
let b = abstract ensures { result <-> _lf = null /\ _rg = null } let b = begin ensures { result <-> _lf = null /\ _rg = null }
ensures { result -> lf = Empty /\ rg = Empty } ensures { result -> lf = Empty /\ rg = Empty }
is_null _lf && is_null _rg end in is_null _lf && is_null _rg end in
if not b then begin if not b then begin
...@@ -394,13 +395,13 @@ module Recursive ...@@ -394,13 +395,13 @@ module Recursive
in in
let ghost mem0 = get_all_accs () in let ghost mem0 = get_all_accs () in
try aux t; try aux t;
'I: label I in
loop while true do
invariant { memo = at memo 'I } invariant { memo = (memo at I) }
invariant { rotated mem0 memo.accessor Finish !x /\ !entered } invariant { rotated mem0 memo.accessor Finish !x /\ !entered }
variant { 0 } variant { 0 }
bloc mem0 Finish bloc mem0 Finish
end done
with Stop -> (ghost ext_cur mem0 t root (null ())); () end with Stop -> (ghost ext_cur mem0 t root (null ())); () end
end end
...@@ -645,7 +646,7 @@ module Iterative ...@@ -645,7 +646,7 @@ module Iterative
let ghost st = ref Bottom in let ghost st = ref Bottom in
ghost opening t t stop stop st; ghost opening t t stop stop st;
let entered = ref false in (* encode do-while loop. *) let entered = ref false in (* encode do-while loop. *)
while not(abstract ensures { result <-> !x = null } while not (begin ensures { result <-> !x = null }
!entered && is_null !x end) !entered && is_null !x end)
do (* ==> do { BODY } while(x != null); *) do (* ==> do { BODY } while(x != null); *)
invariant { !x = null -> !entered } invariant { !x = null -> !entered }
......
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