Commit 4902aafd authored by MARCHE Claude's avatar MARCHE Claude

examples to port (wip)

parent a1e032f6
This source diff could not be displayed because it is too large. You can view the blob instead.
...@@ -21,6 +21,7 @@ module InPlaceRev ...@@ -21,6 +21,7 @@ module InPlaceRev
use import list.List use import list.List
use list.Quant use list.Quant
use import list.Append use import list.Append
use import list.Mem
use import list.Length use import list.Length
use export list.Reverse use export list.Reverse
...@@ -29,9 +30,6 @@ module InPlaceRev ...@@ -29,9 +30,6 @@ module InPlaceRev
val function eq_loc (l1 l2:loc) : bool val function eq_loc (l1 l2:loc) : bool
ensures { result <-> l1 = l2 } ensures { result <-> l1 = l2 }
let function mem (x:loc) (l:list loc) : bool =
Quant.for_some (eq_loc x) l
val constant null : loc val constant null : loc
predicate disjoint (l1:list loc) (l2:list loc) = predicate disjoint (l1:list loc) (l2:list loc) =
...@@ -154,9 +152,11 @@ module InPlaceRev ...@@ -154,9 +152,11 @@ module InPlaceRev
variant { !pM } variant { !pM }
match !pM with match !pM with
| Nil -> absurd | Nil -> absurd
| Cons _ t -> | Cons h t ->
l1pM := !l1pM ++ Cons !p Nil; pM := t;
pM := t assert { disjoint !l1pM !pM };
assert { not (mem h !pM) };
l1pM := !l1pM ++ Cons h Nil;
end; end;
p := acc next !p p := acc next !p
done; done;
...@@ -202,8 +202,8 @@ module InPlaceRevSeq ...@@ -202,8 +202,8 @@ module InPlaceRevSeq
use import int.Int use import int.Int
use map.Map use map.Map
use import seq.Seq use import seq.Seq
use import seq.Mem
use import seq.Reverse use import seq.Reverse
use import ref.Ref
type loc type loc
...@@ -212,9 +212,6 @@ module InPlaceRevSeq ...@@ -212,9 +212,6 @@ module InPlaceRevSeq
val function eq_loc (l1 l2:loc) : bool val function eq_loc (l1 l2:loc) : bool
ensures { result <-> l1 = l2 } ensures { result <-> l1 = l2 }
predicate mem (x: loc) (s: seq loc) =
exists i. 0 <= i < length s /\ eq_loc s[i] x
predicate disjoint (s1: seq 'a) (s2: seq 'a) = predicate disjoint (s1: seq 'a) (s2: seq 'a) =
(* forall x:'a. not (mem x s1 /\ mem x s2) *) (* forall x:'a. not (mem x s1 /\ mem x s2) *)
forall i1. 0 <= i1 < length s1 -> forall i1. 0 <= i1 < length s1 ->
...@@ -239,6 +236,8 @@ module InPlaceRevSeq ...@@ -239,6 +236,8 @@ module InPlaceRevSeq
let (s1, s2) = mem_decomp x s[1 .. ] in (cons s[0] s1, s2) let (s1, s2) = mem_decomp x s[1 .. ] in (cons s[0] s1, s2)
end end
use import ref.Ref
type memory 'a = ref (Map.map loc 'a) type memory 'a = ref (Map.map loc 'a)
val acc (field: memory 'a) (l:loc) : 'a val acc (field: memory 'a) (l:loc) : 'a
......
...@@ -306,6 +306,9 @@ theory Mem ...@@ -306,6 +306,9 @@ theory Mem
predicate mem (x: 'a) (s: seq 'a) = predicate mem (x: 'a) (s: seq 'a) =
exists i: int. 0 <= i < length s && s[i] = x exists i: int. 0 <= i < length s && s[i] = x
lemma mem_append : forall x:'a, s1 s2.
mem x (s1 ++ s2) <-> mem x s1 \/ mem x s2
end end
theory Distinct theory Distinct
......
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