Commit cd95bfe1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fm 2012, pbm 3 (in progress)

parent 804f893a
......@@ -16,26 +16,22 @@ module Memory
type node = { left: pointer; right: pointer; data: int; }
type memory = map pointer node
function get_left (m: memory) (p: pointer) : pointer = (get m p).left
function get_right (m: memory) (p: pointer) : pointer = (get m p).right
function get_data (m: memory) (p: pointer) : int = (get m p).data
(* the global variable mem contains the current state of the memory *)
val mem: ref memory
(* accessor functions to ensure safety i.e. no null pointer dereference *)
let get_left (p: pointer) =
requires { p <> null }
ensures { result = (get !mem p).left }
(get !mem p).left
ensures { result = !mem[p].left }
!mem[p].left
let get_right (p: pointer) =
requires { p <> null }
ensures { result = (get !mem p).right }
(get !mem p).right
ensures { result = !mem[p].right }
!mem[p].right
let get_data (p: pointer) =
requires { p <> null }
ensures { result = (get !mem p).data }
(get !mem p).data
ensures { result = !mem[p].data }
!mem[p].data
end
......@@ -44,7 +40,6 @@ module Treedel
use import Memory
use import bintree.Tree
use import bintree.Inorder
use import bintree.Zipper
use import list.Distinct
(* there is a binary tree t rooted at p in memory m *)
......@@ -52,25 +47,27 @@ module Treedel
| leaf: forall m: memory. tree m null Empty
| node: forall m: memory, p: pointer, l r: tree pointer.
p <> null ->
tree m (get_left m p) l ->
tree m (get_right m p) r ->
tree m m[p].left l ->
tree m m[p].right r ->
tree m p (Node l p r)
(*
lemma frame:
forall m1: memory, p: pointer.
let n = get m1 p in
let m2 = set m1 p { n with left = (get m1 n.left).right } in
forall q: pointer. tree m1 q -> tree m2 q
(* degenerated zipper for a left descent *)
type zipper 'a =
| Top
| Left (zipper 'a) 'a (tree 'a)
function zip (t: tree 'a) (z: zipper 'a) : tree 'a = match z with
| Top -> t
| Left z x r -> zip (Node t x r) z
end
function leaves (m: memory) (p: pointer) : list pointer
lemma inorder_zip:
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))
axiom leaves_null: forall m: memory. leaves m null = Nil
axiom leaves_node:
forall m: memory, p: pointer. tree m p -> p <> null ->
leaves m p =
leaves m (get_left m p) ++ (Cons p Nil) ++ leaves m (get_right m p)
*)
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 }
......@@ -82,45 +79,55 @@ module Treedel
ensures { match t with Empty -> false | Node _ _ r -> result = r end }
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)
(* 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 *)
let search_tree_delete_min
(t: pointer) (ghost x: pointer) (ghost gt: tree pointer) =
(t: pointer) (ghost it: tree pointer) (ghost ot: ref (tree pointer)) =
requires { t <> null }
requires { tree !mem t gt }
requires { match inorder gt with
requires { tree !mem t it }
requires { distinct (inorder it) }
ensures { let (t, m) = result in tree !mem t !ot /\
match inorder it with
| Nil -> false
| Cons p l -> p = x /\ distinct (Cons p l) end }
(*
ensures { let (t, m) = result in
tree !mem t /\ leaves !mem t = l /\ m = get_data !mem x }
*)
| Cons p l -> m = !mem[p].data /\ inorder !ot = l end }
let p = ref (get_left t) in
if !p = null then begin
let m = get_data t in
let tt = get_right t in
ghost match it with Empty -> absurd
| Node l _ r -> assert { l = Empty }; ot := r end;
(tt, m)
end else begin
let pp = ref t in
let tt = ref (get_left !p) in
let ghost zipper = ref (Left Top t (right gt)) in
let ghost subtree = ref (left gt) in
let ghost zipper = ref (Left Top t (right it)) in
let ghost subtree = ref (left it) in
while !tt <> null do
invariant {
(* tree !mem !pp /\
leaves !mem t = leaves !mem !pp ++ !suffix /\ *)
!pp <> null /\ get_left !mem !pp = !p /\
!p <> null /\ get_left !mem !p = !tt }
zipper := Left !zipper !p (right !subtree);
subtree := left !subtree;
invariant { !pp <> null /\ !mem[!pp].left = !p /\
!p <> null /\ !mem[!p].left = !tt /\
tree !mem !p !subtree /\
zip !subtree !zipper = it }
ghost match !subtree with
| Empty -> absurd
| Node l _ r -> zipper := Left !zipper !p r; subtree := l end;
pp := !p;
p := !tt;
tt := get_left !p
done;
assert { !p = x };
let m = get_data !p in
tt := get_right !p;
mem := set !mem !pp { (get !mem !pp) with left = !tt };
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;
(t, m)
end
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
name="Z3"
version="3.2"/>
<file
name="../verifythis_fm2012_treedel.mlw"
verified="false"
expanded="true">
<theory
name="Memory"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="9" loccnumb="7" loccnume="13"
verified="true"
expanded="false">
<goal
name="WP_parameter get_left"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="23" loccnumb="6" loccnume="14"
expl="VC for get_left"
sum="b5175a3787de16d05ce0fb90adf7715c"
proved="true"
expanded="false"
shape="ainfix =aleftagetV1V0aleftagetV1V0Iainfix =V0anullNFF">
<label
name="expl:VC for get_left"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter get_right"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="27" loccnumb="6" loccnume="15"
expl="VC for get_right"
sum="27a9da39fadab55c6a833e0dafb0e443"
proved="true"
expanded="false"
shape="ainfix =arightagetV1V0arightagetV1V0Iainfix =V0anullNFF">
<label
name="expl:VC for get_right"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter get_data"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="31" loccnumb="6" loccnume="14"
expl="VC for get_data"
sum="77819bfc08f5209dc563e4d81a1a974c"
proved="true"
expanded="false"
shape="ainfix =adataagetV1V0adataagetV1V0Iainfix =V0anullNFF">
<label
name="expl:VC for get_data"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="Treedel"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="38" loccnumb="7" loccnume="14"
verified="false"
expanded="true">
<goal
name="inorder_zip"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="64" loccnumb="8" loccnume="19"
sum="9e58b1a0ac813d1cb156465bd483b3b6"
proved="true"
expanded="false"
shape="ainfix =ainorderazipaNodeV2V1V3V0ainfix ++ainorderV2aConsV1ainorderazipV3V0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="false">
<goal
name="inorder_zip.1"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="64" loccnumb="8" loccnume="19"
expl="1."
sum="4f8861704f70f7e4e36ce61051a56380"
proved="true"
expanded="false"
shape="CV0aTopainfix =ainorderazipaNodeV2V1V3V0ainfix ++ainorderV2aConsV1ainorderazipV3V0FaLeftVVVainfix =ainorderazipaNodeV8V7V9V0ainfix ++ainorderV8aConsV7ainorderazipV9V0FIainfix =ainorderazipaNodeV11V10V12V4ainfix ++ainorderV11aConsV10ainorderazipV12V4FF">
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="inorder_zip.1.1"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="64" loccnumb="8" loccnume="19"
expl="1."
sum="19a8e10a34c97930b46443d73184cba9"
proved="true"
expanded="false"
shape="CV0aTopainfix =ainorderazipaNodeV2V1V3V0ainfix ++ainorderV2aConsV1ainorderazipV3V0FaLeftVVVtF">
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="inorder_zip.1.2"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="64" loccnumb="8" loccnume="19"
expl="2."
sum="b4de059965d0d279fb25933cf770df02"
proved="true"
expanded="false"
shape="CV0aToptaLeftVVVainfix =ainorderazipaNodeV5V4V6V0ainfix ++ainorderV5aConsV4ainorderazipV6V0FIainfix =ainorderazipaNodeV8V7V9V1ainfix ++ainorderV8aConsV7ainorderazipV9V1FF">
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.34"/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal
name="zip_bottom_left"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="68" loccnumb="8" loccnume="23"
sum="e153f973d1b6508b776030693cd64564"
proved="true"
expanded="true"
shape="ainfix =ainorderazipaNodeaEmptyV0V1V2aConsV0ainorderazipV1V2F">
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter left"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="72" loccnumb="6" loccnume="10"
expl="VC for left"
sum="d3e0be486058d09fc6108f7a678525be"
proved="true"
expanded="false"
shape="CV0aEmptyfaNodeVwwCV0aEmptyfaNodeVwwainfix =V1V2Iainfix =V0aEmptyNF">
<label
name="expl:VC for left"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter right"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="77" loccnumb="6" loccnume="11"
expl="VC for right"
sum="ca41beddc3a59dc2945cadb0720004fd"
proved="true"
expanded="false"
shape="CV0aEmptyfaNodewwVCV0aEmptyfaNodewwVainfix =V1V2Iainfix =V0aEmptyNF">
<label
name="expl:VC for right"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="main_lemma"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="82" loccnumb="8" loccnume="18"
sum="cd8fe1d5e21d4463daf6b860046ca1c6"
proved="false"
expanded="true"
shape="atreeV7V1azipV4V5Lamixfix [&lt;-]V0V2amk nodearightamixfix []V0V3arightamixfix []V0V2adataamixfix []V0V2Iainfix =aleftamixfix []V0V2V3IadistinctainorderV6IatreeV0V1V6LazipaNodeaEmptyV3V4V5F">
</goal>
<goal
name="WP_parameter search_tree_delete_min"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="VC for search_tree_delete_min"
sum="fd0a5d94368635d618faf242246b7978"
proved="true"
expanded="true"
shape="iainfix =aleftagetV2V0anullCV1aEmptyfaNodeVwVCainorderV1aNilfaConsVVainfix =ainorderV5V7Aainfix =adataagetV2V0adataagetV2V6AatreeV2arightagetV2V0V5Iainfix =V5V4FAainfix =V3aEmptyAainfix =V0anullNAainfix =V0anullNiainfix =V13anullNCV11aEmptyfaNodeVwVainfix =azipV19V18V1AatreeV2V21V19Aainfix =aleftagetV2V21V22Aainfix =V21anullNAainfix =aleftagetV2V20V21Aainfix =V20anullNIainfix =V22aleftagetV2V21FAainfix =V21anullNIainfix =V21V13FIainfix =V20V15FIainfix =V19V16FIainfix =V18aLeftV12V15V17FCV11aEmptyfaNodeVwVCainorderV1aNilfaConsVVainfix =ainorderV27V29Aainfix =adataagetV2V15adataagetV24V28AatreeV24V0V27Iainfix =V27azipV26V12FAainfix =V25aEmptyIainfix =V24asetV2V14amk nodeV23arightagetV2V14adataagetV2V14FIainfix =V23arightagetV2V15FAainfix =V15anullNAainfix =V15anullNIainfix =azipV11V12V1AatreeV2V15V11Aainfix =aleftagetV2V15V13Aainfix =V15anullNAainfix =aleftagetV2V14V15Aainfix =V14anullNFAainfix =azipV10aLeftaTopV0V9V1AatreeV2aleftagetV2V0V10Aainfix =aleftagetV2aleftagetV2V0aleftagetV2V8Aainfix =aleftagetV2V0anullNAainfix =aleftagetV2V0aleftagetV2V0Aainfix =V0anullNICV1aEmptyfaNodeVwwainfix =V10V30FAainfix =V1aEmptyNICV1aEmptyfaNodewwVainfix =V9V31FAainfix =V1aEmptyNAainfix =V8anullNLaleftagetV2V0Aainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
<goal
name="WP_parameter search_tree_delete_min.1"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="1. precondition"
sum="fbb1867b56ed8c7dc3c1725df7efd4f5"
proved="true"
expanded="false"
shape="ainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter search_tree_delete_min.2"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="2. precondition"
sum="177b46b5efdc6639b5a6037d634cd5ed"
proved="true"
expanded="false"
shape="ainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter search_tree_delete_min.3"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="3. precondition"
sum="f3396600c365b8efa18b54fb5d6bc6b0"
proved="true"
expanded="false"
shape="ainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter search_tree_delete_min.4"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="4."
sum="276e0fc816bc1753323e66abf8d90a84"
proved="true"
expanded="false"
shape="CV1aEmptyfaNodeVwVtIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter search_tree_delete_min.4.1"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="1."
sum="276e0fc816bc1753323e66abf8d90a84"
proved="true"
expanded="false"
shape="CV1aEmptyfaNodeVwVtIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter search_tree_delete_min.5"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="5. assertion"
sum="485c0676c73cca5d9cdf815808e0abe2"
proved="true"
expanded="false"
shape="CV1aEmptytaNodeVwVainfix =V3aEmptyIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter search_tree_delete_min.5.1"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="1. assertion"
sum="485c0676c73cca5d9cdf815808e0abe2"
proved="true"
expanded="false"
shape="CV1aEmptytaNodeVwVainfix =V3aEmptyIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter search_tree_delete_min.6"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="6. postcondition"
sum="959b3088a0c984d5f448615142e252be"
proved="true"
expanded="false"
shape="CV1aEmptytaNodeVwVCainorderV1aNilfaConsVVainfix =ainorderV5V7Aainfix =adataagetV2V0adataagetV2V6AatreeV2arightagetV2V0V5Iainfix =V5V4FIainfix =V3aEmptyIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter search_tree_delete_min.6.1"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="1."
sum="4522ad643a9ec29a6ed4a828891652ad"
proved="true"
expanded="false"
shape="CV1aEmptytaNodeVwVatreeV2arightagetV2V0V5Iainfix =V5V4FIainfix =V3aEmptyIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter search_tree_delete_min.6.2"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="2."
sum="8ad348a4ff23c09c6045e234ed029bf8"
proved="true"
expanded="false"
shape="CV1aEmptytaNodeVwVCainorderV1aNilfaConsVVtIainfix =V5V4FIainfix =V3aEmptyIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal
name="WP_parameter search_tree_delete_min.6.3"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="3."
sum="d8f27d733e3182b17bb7ec484ef415de"
proved="true"
expanded="false"
shape="CV1aEmptytaNodeVwVCainorderV1aNiltaConsVVainfix =adataagetV2V0adataagetV2V6Iainfix =V5V4FIainfix =V3aEmptyIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label
name="expl:VC for search_tree_delete_min"/>
<proof
prover="0"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.99"/>
</proof>
</goal>
<goal
name="WP_parameter search_tree_delete_min.6.4"
locfile="../verifythis_fm2012_treedel.mlw"
loclnum="93" loccnumb="6" loccnume="28"
expl="4."
sum="a8cd3d87413368850600b6ab4775eb14"
proved="true"
expanded="false"
shape="CV1aEmptytaNodeVwVCainorderV1aNiltaConsVVainfix =ainorderV5V7Iainfix =V5V4FIainfix =V3aEmptyIainfix =V0anullNIainfix =V0anullNIainfix =aleftagetV2V0anullIainfix =V0anullNIadistinctainorderV1AatreeV2V0V1Aainfix =V0anullNFF">
<label