Commit 64120027 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update session

parent 7f18b955
......@@ -2,35 +2,11 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require map.Map.
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).
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
......@@ -40,7 +16,7 @@ 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 :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
......@@ -52,32 +28,34 @@ Existing Instance pointer_WhyType.
Parameter null: pointer.
(* Why3 assumption *)
Inductive node :=
| mk_node : pointer -> pointer -> Z -> node .
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
Definition data (v:node): Z := match v with
| (mk_node x x1 x2) => x2
end.
(* Why3 assumption *)
Definition right1(v:node): pointer :=
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
Definition left1 (v:node): pointer :=
match v with
| (mk_node x x1 x2) => x
end.
(* Why3 assumption *)
Definition memory := (map pointer node).
Definition memory := (map.Map.map pointer node).
(* Why3 assumption *)
Inductive tree (a:Type) {a_WT:WhyType a} :=
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).
......@@ -86,7 +64,8 @@ Implicit Arguments Empty [[a] [a_WT]].
Implicit Arguments Node [[a] [a_WT]].
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
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).
......@@ -95,7 +74,7 @@ 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
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
......@@ -110,7 +89,7 @@ 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 :=
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
......@@ -127,7 +106,7 @@ Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
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)
......@@ -142,7 +121,7 @@ Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint inorder {a:Type} {a_WT:WhyType a}(t:(tree a)) {struct t}: (list
Fixpoint inorder {a:Type} {a_WT:WhyType a} (t:(tree a)) {struct t}: (list
a) :=
match t with
| Empty => (Nil :(list a))
......@@ -153,23 +132,26 @@ Fixpoint inorder {a:Type} {a_WT:WhyType a}(t:(tree a)) {struct t}: (list
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))).
| 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)))).
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
Inductive tree1 : (map.Map.map pointer node) -> pointer -> (tree
pointer) -> Prop :=
| leaf : forall (m:(map.Map.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)))).
| node1 : forall (m:(map.Map.map pointer node)) (p:pointer) (l:(tree
pointer)) (r:(tree pointer)), (~ (p = null)) -> ((tree1 m
(left1 (map.Map.get m p)) l) -> ((tree1 m (right1 (map.Map.get m p))
r) -> (tree1 m p (Node l p r)))).
(* Why3 assumption *)
Inductive zipper (a:Type) {a_WT:WhyType a} :=
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).
......@@ -178,7 +160,7 @@ 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
Fixpoint zip {a:Type} {a_WT:WhyType a} (t:(tree a)) (z:(zipper
a)) {struct z}: (tree a) :=
match z with
| Top => t
......@@ -189,22 +171,23 @@ 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 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))))).
Axiom main_lemma : forall (m:(map.Map.map pointer node)) (t:pointer)
(pp:pointer) (p:pointer) (ppr:(tree pointer)) (pr:(tree pointer))
(z:(zipper pointer)), let it := (zip (Node (Node (Empty :(tree pointer)) p
pr) pp ppr) z) in ((tree1 m t it) -> ((distinct (inorder it)) -> (tree1
(map.Map.set m pp (mk_node (right1 (map.Map.get m p))
(right1 (map.Map.get m pp)) (data (map.Map.get m pp)))) t (zip (Node pr pp
ppr) z)))).
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)) /\
pointer)), forall (mem1:(map.Map.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
((~ ((left1 (map.Map.get mem1 t)) = null)) -> ((~ ((left1 (map.Map.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)),
......@@ -213,14 +196,16 @@ Theorem WP_parameter_search_tree_delete_min : forall (t:pointer) (it:(tree
| (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))))) ->
((~ (subtree = (Empty :(tree pointer)))) -> forall (pl:(tree pointer)),
((((~ (pp = null)) /\ ((left1 (map.Map.get mem1 pp)) = p)) /\
((~ (p = null)) /\ ((left1 (map.Map.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 (map.Map.get mem1 p))) ->
forall (mem2:(map.Map.map pointer node)), (mem2 = (map.Map.set mem1 pp
(mk_node tt1 (right1 (map.Map.get mem1 pp)) (data (map.Map.get mem1
pp))))) -> ((~ (subtree = (Empty :(tree pointer)))) -> forall (pl:(tree
pointer)),
match subtree with
| Empty => False
| (Node l _ _) => (pl = l)
......@@ -234,8 +219,9 @@ Theorem WP_parameter_search_tree_delete_min : forall (t:pointer) (it:(tree
| Nil => True
| (Cons p1 l) => ((inorder ot) = l)
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.
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.
intuition.
intros.
......
......@@ -309,7 +309,7 @@
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="71" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
expanded="true">
<goal
name="inorder_zip"
locfile="../verifythis_fm2012_treedel.mlw"
......@@ -768,14 +768,14 @@
expl="VC for search_tree_delete_min"
sum="91569afc812057a9c9998241542f6be7"
proved="true"
expanded="false"
expanded="true"
shape="iainfix =aleftagetV2V0anullCV1aEmptyfaNodeVwVCainorderV1aNilfaConsVVainfix =ainorderV5V7Aainfix =adataagetV2V0adataagetV2V6AatreeV2arightagetV2V0V5Iainfix =V5V4FAainfix =V3aEmptyAainfix =V0anullNAainfix =V0anullNiainfix =V14anullNainfix =azipV25V17V1AatreeV2V22V25LaNodeV21V22V19Aainfix =aleftagetV2V23V24Aainfix =V23anullNAainfix =aleftagetV2V22V23Aainfix =V22anullNIainfix =V24aleftagetV2V23FAainfix =V23anullNIainfix =V23V14FIainfix =V22V16FIainfix =V21V20FICV11aEmptyfaNodeVwwainfix =V20V26FAainfix =V11aEmptyNIainfix =V19V18FICV11aEmptyfaNodewwVainfix =V18V27FAainfix =V11aEmptyNIainfix =V17aLeftV13V15V12FAatreeV2V16V11CainorderV1aNilfaConsVVainfix =ainorderV32V34Aainfix =adataagetV2V16adataagetV29V33AatreeV29V0V32Iainfix =V32azipV31aLeftV13V15V12FICV11aEmptyfaNodewwVainfix =V31V35FAainfix =V11aEmptyNAainfix =V30aEmptyICV11aEmptyfaNodeVwwainfix =V30V36FAainfix =V11aEmptyNIainfix =V29asetV2V15amk nodeV28arightagetV2V15adataagetV2V15FIainfix =V28arightagetV2V16FAainfix =V16anullNAainfix =V16anullNAainfix =V15V16NAatreeV2V16V11Iainfix =azipV37V13V1AatreeV2V15V37LaNodeV11V15V12Aainfix =aleftagetV2V16V14Aainfix =V16anullNAainfix =aleftagetV2V15V16Aainfix =V15anullNFAainfix =azipV38aTopV1AatreeV2V0V38LaNodeV10V0V9Aainfix =aleftagetV2aleftagetV2V0aleftagetV2V8Aainfix =aleftagetV2V0anullNAainfix =aleftagetV2V0aleftagetV2V0Aainfix =V0anullNICV1aEmptyfaNodeVwwainfix =V10V39FAainfix =V1aEmptyNICV1aEmptyfaNodewwVainfix =V9V40FAainfix =V1aEmptyNAainfix =V8anullNLaleftagetV2V0Aainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter search_tree_delete_min.1"
locfile="../verifythis_fm2012_treedel.mlw"
......@@ -1215,14 +1215,6 @@
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="0.69"/>
</proof>
<proof
prover="2"
timelimit="5"
......@@ -2967,14 +2959,14 @@
expl="27. postcondition"
sum="1576f78220ecb6258d1c6c3f73b5e9de"
proved="true"
expanded="false"
expanded="true"
shape="CainorderV1aNilfaConsVVainfix =ainorderV16V18Aainfix =adataagetV2V11adataagetV13V17AatreeV13V0V16Iainfix =V16azipV15aLeftV8V10V7FICV6aEmptyfaNodewwVainfix =V15V19FIainfix =V6aEmptyNIainfix =V14aEmptyICV6aEmptyfaNodeVwwainfix =V14V20FIainfix =V6aEmptyNIainfix =V13asetV2V10amk nodeV12arightagetV2V10adataagetV2V10FIainfix =V12arightagetV2V11FIainfix =V11anullNIainfix =V11anullNIainfix =V10V11NIatreeV2V11V6Iainfix =V9anullNNIainfix =azipV21V8V1AatreeV2V10V21LaNodeV6V10V7Aainfix =aleftagetV2V11V9Aainfix =V11anullNAainfix =aleftagetV2V10V11Aainfix =V10anullNFICV1aEmptyfaNodeVwwainfix =V5V22FIainfix =V1aEmptyNICV1aEmptyfaNodewwVainfix =V4V23FIainfix =V1aEmptyNIainfix =V3anullNLaleftagetV2V0Iainfix =aleftagetV2V0anullNIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter search_tree_delete_min.27.1"
locfile="../verifythis_fm2012_treedel.mlw"
......@@ -3150,7 +3142,7 @@
expl="3."
sum="5097560114a248e32ec7fcb79c62c1b7"
proved="true"
expanded="false"
expanded="true"
shape="CainorderV1aNiltaConsVVainfix =adataagetV2V11adataagetV13V17Iainfix =V16azipV15aLeftV8V10V7FICV6aEmptyfaNodewwVainfix =V15V19FIainfix =V6aEmptyNIainfix =V14aEmptyICV6aEmptyfaNodeVwwainfix =V14V20FIainfix =V6aEmptyNIainfix =V13asetV2V10amk nodeV12arightagetV2V10adataagetV2V10FIainfix =V12arightagetV2V11FIainfix =V11anullNIainfix =V11anullNIainfix =V10V11NIatreeV2V11V6Iainfix =V9anullNNIainfix =azipV21V8V1AatreeV2V10V21LaNodeV6V10V7Aainfix =aleftagetV2V11V9Aainfix =V11anullNAainfix =aleftagetV2V10V11Aainfix =V10anullNFICV1aEmptyfaNodeVwwainfix =V5V22FIainfix =V1aEmptyNICV1aEmptyfaNodewwVainfix =V4V23FIainfix =V1aEmptyNIainfix =V3anullNLaleftagetV2V0Iainfix =aleftagetV2V0anullNIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
......@@ -3194,14 +3186,6 @@
archived="false">
<result status="timeout" time="56.46"/>
</proof>
<proof
prover="5"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="22.61"/>
</proof>
<proof
prover="7"
timelimit="60"
......@@ -3234,7 +3218,7 @@
expl="4."
sum="3589cdddc12e68f4e0d2c6fb1f8921b3"
proved="true"
expanded="false"
expanded="true"
shape="CainorderV1aNiltaConsVVainfix =ainorderV16V18Iainfix =V16azipV15aLeftV8V10V7FICV6aEmptyfaNodewwVainfix =V15V19FIainfix =V6aEmptyNIainfix =V14aEmptyICV6aEmptyfaNodeVwwainfix =V14V20FIainfix =V6aEmptyNIainfix =V13asetV2V10amk nodeV12arightagetV2V10adataagetV2V10FIainfix =V12arightagetV2V11FIainfix =V11anullNIainfix =V11anullNIainfix =V10V11NIatreeV2V11V6Iainfix =V9anullNNIainfix =azipV21V8V1AatreeV2V10V21LaNodeV6V10V7Aainfix =aleftagetV2V11V9Aainfix =V11anullNAainfix =aleftagetV2V10V11Aainfix =V10anullNFICV1aEmptyfaNodeVwwainfix =V5V22FIainfix =V1aEmptyNICV1aEmptyfaNodewwVainfix =V4V23FIainfix =V1aEmptyNIainfix =V3anullNLaleftagetV2V0Iainfix =aleftagetV2V0anullNIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
......@@ -3293,7 +3277,7 @@
edited="verifythis_fm2012_treedel_Treedel_WP_parameter_search_tree_delete_min_2.v"
obsolete="false"
archived="false">
<result status="valid" time="1.18"/>
<result status="valid" time="0.77"/>
</proof>
<proof
prover="7"
......
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