fm 2012, pbm 3 (spec simplification)

parent cd95bfe1
......@@ -5,7 +5,7 @@
Author: Jean-Christophe Filliâtre *)
(* Why3 has no pointer data structures, so we model it *)
(* Why3 has no pointer data structures, so we model the heap *)
module Memory
use export map.Map
......@@ -44,7 +44,8 @@ module Treedel
(* there is a binary tree t rooted at p in memory m *)
inductive tree (m: memory) (p: pointer) (t: tree pointer) =
| leaf: forall m: memory. tree m null Empty
| leaf: forall m: memory.
tree m null Empty
| node: forall m: memory, p: pointer, l r: tree pointer.
p <> null ->
tree m m[p].left l ->
......@@ -65,10 +66,6 @@ module Treedel
forall z "induction": zipper 'a, x: 'a, l r: tree 'a.
inorder (zip (Node l x r) z) = inorder l ++ Cons x (inorder (zip r z))
lemma zip_bottom_left:
forall x: 'a, r: tree 'a, z: zipper 'a.
inorder (zip (Node Empty x r) z) = Cons x (inorder (zip r z))
let left (t: tree pointer) =
requires { t <> Empty }
ensures { match t with Empty -> false | Node l _ _ -> result = l end }
......@@ -80,13 +77,11 @@ module Treedel
match t with Empty -> absurd | Node _ _ r -> r end
lemma main_lemma:
forall m: memory, t pp p: pointer, r: tree pointer, z: zipper pointer.
let it = zip (Node Empty p r) z in
tree m t it ->
distinct (inorder it) ->
m[pp].left = p ->
let m' = m[pp <- { m[pp] with left = m[p].right }] in
tree m' t (zip r z)
forall m: memory, t pp p: pointer, ppr pr: tree pointer, z: zipper pointer.
let it = zip (Node Empty p pr) (Left z pp ppr) in
tree m t it -> distinct (inorder it) ->
let m' = m[pp <- { m[pp] with left = m[p].right }] in
tree m' t (zip pr (Left z pp ppr))
(* specification is as follows: if t is a tree and its list of pointers
is x::l then, at the end of execution, its list is l and m = x.data *)
......@@ -109,25 +104,31 @@ module Treedel
end else begin
let pp = ref t in
let tt = ref (get_left !p) in
let ghost zipper = ref (Left Top t (right it)) in
let ghost zipper = ref Top in
let ghost ppr = ref (right it) in
let ghost subtree = ref (left it) in
while !tt <> null do
invariant { !pp <> null /\ !mem[!pp].left = !p /\
!p <> null /\ !mem[!p].left = !tt /\
tree !mem !p !subtree /\
zip !subtree !zipper = it }
let pt = Node !subtree !pp !ppr in
tree !mem !pp pt /\ zip pt !zipper = it }
assert { tree !mem !p !subtree };
ghost zipper := Left !zipper !pp !ppr;
ghost match !subtree with
| Empty -> absurd
| Node l _ r -> zipper := Left !zipper !p r; subtree := l end;
| Node l _ r -> ppr := r; subtree := l end;
pp := !p;
p := !tt;
tt := get_left !p
done;
assert { tree !mem !p !subtree };
assert { !pp <> !p };
let m = get_data !p in
tt := get_right !p;
mem := set !mem !pp { !mem[!pp] with left = !tt };
ghost match !subtree with Empty -> absurd
| Node l _ r -> assert { l = Empty }; ot := zip r !zipper end;
| Node pl _ pr ->
assert { pl = Empty }; ot := zip pr (Left !zipper !pp !ppr) end;
(t, m)
end
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Axiom pointer : Type.
Parameter pointer_WhyType : WhyType pointer.
Existing Instance pointer_WhyType.
Parameter null: pointer.
(* Why3 assumption *)
Inductive node :=
| mk_node : pointer -> pointer -> Z -> node .
Axiom node_WhyType : WhyType node.
Existing Instance node_WhyType.
(* Why3 assumption *)
Definition data(v:node): Z := match v with
| (mk_node x x1 x2) => x2
end.
(* Why3 assumption *)
Definition right1(v:node): pointer :=
match v with
| (mk_node x x1 x2) => x1
end.
(* Why3 assumption *)
Definition left1(v:node): pointer := match v with
| (mk_node x x1 x2) => x
end.
(* Why3 assumption *)
Definition memory := (map pointer node).
(* Why3 assumption *)
Inductive tree (a:Type) {a_WT:WhyType a} :=
| Empty : tree a
| Node : (tree a) -> a -> (tree a) -> tree a.
Axiom tree_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (tree a).
Existing Instance tree_WhyType.
Implicit Arguments Empty [[a] [a_WT]].
Implicit Arguments Node [[a] [a_WT]].
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint inorder {a:Type} {a_WT:WhyType a}(t:(tree a)) {struct t}: (list
a) :=
match t with
| Empty => (Nil :(list a))
| (Node l x r) => (infix_plpl (inorder l) (Cons x (inorder r)))
end.
(* Why3 assumption *)
Inductive distinct{a:Type} {a_WT:WhyType a} : (list a) -> Prop :=
| distinct_zero : (distinct (Nil :(list a)))
| distinct_one : forall (x:a), (distinct (Cons x (Nil :(list a))))
| distinct_many : forall (x:a) (l:(list a)), (~ (mem x l)) ->
((distinct l) -> (distinct (Cons x l))).
Axiom distinct_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
a)) (l2:(list a)), (distinct l1) -> ((distinct l2) -> ((forall (x:a),
(mem x l1) -> ~ (mem x l2)) -> (distinct (infix_plpl l1 l2)))).
(* Why3 assumption *)
Inductive tree1 : (map pointer node) -> pointer -> (tree pointer) -> Prop :=
| leaf : forall (m:(map pointer node)), (tree1 m null (Empty :(tree
pointer)))
| node1 : forall (m:(map pointer node)) (p:pointer) (l:(tree pointer))
(r:(tree pointer)), (~ (p = null)) -> ((tree1 m (left1 (get m p)) l) ->
((tree1 m (right1 (get m p)) r) -> (tree1 m p (Node l p r)))).
(* Why3 assumption *)
Inductive zipper (a:Type) {a_WT:WhyType a} :=
| Top : zipper a
| Left : (zipper a) -> a -> (tree a) -> zipper a.
Axiom zipper_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (zipper a).
Existing Instance zipper_WhyType.
Implicit Arguments Top [[a] [a_WT]].
Implicit Arguments Left [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint zip {a:Type} {a_WT:WhyType a}(t:(tree a)) (z:(zipper
a)) {struct z}: (tree a) :=
match z with
| Top => t
| (Left z1 x r) => (zip (Node t x r) z1)
end.
Axiom inorder_zip : forall {a:Type} {a_WT:WhyType a}, forall (z:(zipper a))
(x:a) (l:(tree a)) (r:(tree a)), ((inorder (zip (Node l x r)
z)) = (infix_plpl (inorder l) (Cons x (inorder (zip r z))))).
Axiom zip_bottom_left : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(r:(tree a)) (z:(zipper a)), ((inorder (zip (Node (Empty :(tree a)) x r)
z)) = (Cons x (inorder (zip r z)))).
Axiom main_lemma : forall (m:(map pointer node)) (t:pointer) (pp:pointer)
(p:pointer) (ppr:(tree pointer)) (pr:(tree pointer)) (z:(zipper pointer)),
let it := (zip (Node (Empty :(tree pointer)) p pr) (Left z pp ppr)) in
((tree1 m t it) -> ((distinct (inorder it)) -> (tree1 (set m pp
(mk_node (right1 (get m p)) (right1 (get m pp)) (data (get m pp)))) t
(zip pr (Left z pp ppr))))).
Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_search_tree_delete_min : forall (t:pointer) (it:(tree
pointer)), forall (mem1:(map pointer node)), (((~ (t = null)) /\
(tree1 mem1 t it)) /\ (distinct (inorder it))) -> ((~ (t = null)) ->
((~ ((left1 (get mem1 t)) = null)) -> ((~ ((left1 (get mem1 t)) = null)) ->
((~ (it = (Empty :(tree pointer)))) -> forall (o:(tree pointer)),
match it with
| Empty => False
| (Node _ _ r) => (o = r)
end -> ((~ (it = (Empty :(tree pointer)))) -> forall (o1:(tree pointer)),
match it with
| Empty => False
| (Node l _ _) => (o1 = l)
end -> forall (subtree:(tree pointer)) (ppr:(tree pointer))
(zipper1:(zipper pointer)) (tt:pointer) (pp:pointer) (p:pointer),
((~ (pp = null)) /\ (((left1 (get mem1 pp)) = p) /\ ((~ (p = null)) /\
(((left1 (get mem1 p)) = tt) /\ let pt := (Node subtree pp ppr) in
((tree1 mem1 pp pt) /\ ((zip pt zipper1) = it)))))) -> ((tt = null) ->
((tree1 mem1 p subtree) -> ((~ (pp = p)) -> ((~ (p = null)) ->
((~ (p = null)) -> forall (tt1:pointer), (tt1 = (right1 (get mem1 p))) ->
forall (mem2:(map pointer node)), (mem2 = (set mem1 pp (mk_node tt1
(right1 (get mem1 pp)) (data (get mem1 pp))))) ->
match subtree with
| Empty => True
| (Node pl _ pr) => (pl = (Empty :(tree pointer))) -> forall (ot:(tree
pointer)), (ot = (zip pr (Left zipper1 pp ppr))) ->
match (inorder it) with
| Nil => True
| (Cons p1 l) => ((inorder ot) = l)
end
end)))))))))).
intros t it mem1 ((h1,h2),h3) h4 h5 h6 h7 o h8 h9 o1 h10 subtree ppr zipper1
tt pp p (h11,(h12,(h13,(h14,h15)))) h16 h17 h18 h19 h20 tt1 h21 mem2 h22.
destruct subtree; auto.
intros.
subst subtree1; simpl in h15.
intuition.
rewrite <- H1.
rewrite inorder_zip.
simpl.
ae.
Qed.
......@@ -7,12 +7,11 @@ theory Tree
end
theory Size
theory Size "number of nodes"
use export Tree
use export int.Int
(* number of nodes *)
function size (t: tree 'a) : int = match t with
| Empty -> 0
| Node l _ r -> 1 + size l + size r
......
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