Commit 0455e6a6 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix some typing errors in examples.

parent 66507901
......@@ -33,18 +33,22 @@ module RemoveDuplicateQuadratic
use import Spec
use import ref.Refint
let rec test_appears (ghost w: ref int) (v: 'a) (a: array 'a) (s: int) : bool
type t
val predicate eq (x y: t)
ensures { result <-> x = y }
let rec test_appears (ghost w: ref int) (v: t) (a: array t) (s: int) : bool
requires { 0 <= s <= length a }
ensures { result=true <-> appears v a s }
ensures { result=true -> 0 <= !w < s && a[!w] = v }
ensures { result <-> appears v a s }
ensures { result -> 0 <= !w < s && a[!w] = v }
variant { s }
= s > 0 &&
if a[s-1] = v then begin w := s - 1; true end else test_appears w v a (s-1)
if eq a[s-1] v then begin w := s - 1; true end else test_appears w v a (s-1)
let remove_duplicate (a: array 'a) : int
let remove_duplicate (a: array t): int
ensures { 0 <= result <= length a }
ensures { nodup a result }
ensures { forall v:'a. appears v (old a) (length a) <-> appears v a result }
ensures { forall v. appears v (old a) (length a) <-> appears v a result }
= let n = length a in
let r = ref 0 in
let ghost from = make n 0 in
......
......@@ -6,17 +6,21 @@
module TortoiseAndHare
use import int.Int
use int.Iter
(* let f be a function from t to t *)
type t
function f t : t
val predicate eq (x y : t)
ensures { result <-> x = y }
(* let f be a function from t to t *)
val function f t : t
(* given some initial value x0 *)
constant x0: t
val constant x0: t
(* we can build the infinite sequence defined by x{i+1} = f(xi) *)
clone import int.Iter with type t = t, function f = f
function x (i: int): t = iter i x0
function x (i: int): t = Iter.iter f i x0
(* let use assume now that the sequence (x_i) has finitely many distinct
values (e.g. f is an integer function with values in 0..m)
......@@ -69,7 +73,7 @@ module TortoiseAndHare
let tortoise_hare () =
let tortoise = ref (f x0) in
let hare = ref (f (f x0)) in
while !tortoise <> !hare do
while not (eq !tortoise !hare) do
invariant {
exists t: int.
1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\
......
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