Commit f714743d authored by Martin Clochard's avatar Martin Clochard

avl example (WIP)

Freeze the most generic development, which cannot be finished
in why3 yet.
parent 0cb14a43
(* avl-based random-access lists. *)
module RAL
use import int.Int
use import list.NthLengthAppend
use import avl.SelectionTypes
(* Data is trivial (random-access lists are fully polymorphic). *)
namespace Data
type t 'a 'b = 'a
type m 'a 'b = 'a
predicate c (x:'a) = true
function m (x:'a) : 'a = x
end
(* Tree structure. Store additional information for fast index selection. *)
namespace Tree
use import avl.ParamsTypes
(* Store cardinal at every node. *)
type t 'a 'b =
| TEmpty
| TNode (t 'a 'b) 'a int (t 'a 'b) int
function m (t:t 'a 'b) : m_base (Data.m 'a 'b) = match t with
| TEmpty -> Empty
| TNode l d _ r h -> Node (m l) d.Data.m (m r) h
end
function cardinal (t:m_base (Data.m 'a 'b)) : int = match t with
| Empty -> 0
| Node l _ r _ -> cardinal l + cardinal r + 1
end
predicate c (t:t 'a 'b) = match t with
| TEmpty -> true
| TNode l d card r _ -> Data.c d /\ card = cardinal t.m /\ c l /\ c r
end
(* Those clones cannot be done yet... *)
let empty () : t 'a 'b
ensures { result.m = Empty }
ensures { c result }
= TEmpty
let cardinal (t:t 'a 'b) : int
requires { c t }
ensures { result = cardinal t.m }
= match t with TEmpty -> 0 | TNode _ _ c _ _ -> c end
let node (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) (h:int) : t 'a 'b
requires { c l /\ Data.c d /\ c r }
ensures { result.m = Node l.m d.Data.m r.m h }
ensures { c result }
= TNode l d (cardinal l + cardinal r + 1) r h
let view (t:t 'a 'b) : view_base (t 'a 'b) (Data.t 'a 'b)
ensures { match result with
| VEmpty -> t.m = Empty
| VNode l d r h -> t.m = Node l.m d.Data.m r.m h /\
c l /\ Data.c d /\ c r
end }
= match t with TEmpty -> VEmpty | TNode l d _ r h -> VNode l d r h end
end
namespace S
type t 'a 'b = int
type m 'a 'b = int
predicate c (x:int) = true
function m (x:int) : int = x
end
predicate selector_correct (s:S.m 'a 'b) (l:list (Data.m 'a 'b)) =
0 <= s < length l
predicate selected (s:S.m 'a 'b) (e:position_base (Data.m 'a 'b)) =
length e.left = s /\ match e.middle with
| None -> e.right = Nil
| _ -> true
end
clone import avl.Selection as Sel with namespace P.Data = Data,
namespace S = S, predicate selector_correct = selector_correct,
predicate selected = selected,
goal selector_correct_empty
(* This clone cannot be done yet... *)
let selected_way (s:S.t 'a 'b)
(l:t 'a 'b) (d:P.Data.t 'a 'b) (r:t 'a 'b) : way 'a 'b
requires { l.m.inv = r.m.inv }
requires { Data.c d /\ l.m.inv d.Data.m }
requires { c l /\ c r /\ S.c s }
requires { selector_correct s.S.m (node_model l.m.lis d.P.Data.m r.m.lis) }
(* A selected position can be found by following the given way. *)
returns { Here -> selected s.S.m { left = l.m.lis;
middle = Some d.Data.m;
right = r.m.lis }
| Left sl -> selector_correct sl.S.m l.m.lis /\ S.c sl /\
forall e. selected sl.S.m e ->
selected s.S.m { e with right = node_model e.right d.Data.m r.m.lis }
| Right sr -> selector_correct sr.S.m r.m.lis /\ S.c sr /\
forall e. selected sr.S.m e ->
selected s.S.m { e with left = node_model l.m.lis d.Data.m e.left } }
= let cl = cardinal l in
if s < cl
then Left s
else if s > cl
then Right s
else Here
end
(* Association lists. *)
(* Association with respect to an equivalence relation. *)
module Assoc
clone import key_type.KeyType as K
clone import relations_params.EquivalenceParam as Eq with type t = key
use import list.List
use import list.Mem
use import option.Option
use import HighOrd
predicate appear (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) =
exists x. mem x l /\ correct_for p k /\ Eq.rel p k (key x)
(* Correction. *)
predicate correct (p:param 'a) (l:list (t 'a 'b)) = match l with
| Nil -> true
| Cons x q -> let kx = key x in correct_for p kx /\ correct p q
end
(* Unique occurence (a desirable property of an association list). *)
predicate unique (p:param 'a) (l:list (t 'a 'b)) = match l with
| Nil -> true
| Cons x q -> not appear p (key x) q /\ unique p q
end
(* functional update with equivalence classes. *)
function param_update (p:param 'a) (f:key 'a -> 'b)
(k:key 'a) (b:'b) : key 'a -> 'b = \k2.
if Eq.rel p k k2 then b else f k2
(* functional model of an association list. *)
function model (p:param 'a) (l:list (t 'a 'b)) : key 'a -> option (t 'a 'b) =
match l with
| Nil -> \x. None
| Cons d q -> param_update p (model p q) (key d) (Some d)
end
(* A key is bound iff it occurs in the association lists. *)
let rec lemma model_occurence (p:param 'a) (k:key 'a)
(l:list (t 'a 'b)) : unit
requires { correct p l }
requires { correct_for p k }
ensures { appear p k l <-> match model p l k with None -> false
| Some _ -> true end }
variant { l }
= match l with Cons _ q -> model_occurence p k q | _ -> () end
(* A key is bound to a value with an equivalent key. *)
let rec lemma model_link (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit
requires { correct p l }
requires { correct_for p k }
ensures { match model p l k with None -> true
| Some d -> Eq.rel p k (key d) end }
variant { l }
= match l with Cons _ q -> model_link p k q | _ -> () end
(* Two equivalent keys are bound to the same value. *)
let rec lemma model_equal (p:param 'a) (k1 k2:key 'a)
(l:list (t 'a 'b)) : unit
requires { correct p l }
requires { correct_for p k1 /\ correct_for p k2 }
requires { Eq.rel p k1 k2 }
ensures { model p l k1 = model p l k2 }
variant { l }
= match l with Cons _ q -> model_equal p k1 k2 q | _ -> () end
(* If the list satisfies the uniqueness property,
then every value occuring in the list is the image of its key. *)
let rec lemma model_unique (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit
requires { correct p l }
requires { unique p l }
requires { correct_for p k }
ensures { forall d. mem d l -> model p l (key d) = Some d }
variant { l }
= match l with Cons _ q -> model_unique p k q | _ -> () end
end
(* Sorted (increasing) association list. *)
module AssocSorted
use import list.List
use import list.Append
use import list.Mem
use import option.Option
clone import key_type.KeyType as K
clone import preorder.FullParam as O with type t = key
(* The commented out part do not work, unfortunately. *)
clone export Assoc with namespace K = K,(*namespace Eq = O.Eq*)
type Eq.param = O.order,
predicate Eq.correct_for = O.correct_for,
predicate Eq.rel = O.eq,
(* Duplicates, there is no need to keep them. *)
goal Eq.trans,
goal Eq.refl,
goal Eq.symm
clone sorted.Increasing as S with namespace K = K,
(*namespace O = O.Lt*)
type O.param = O.order,
predicate O.correct_for = O.correct_for,
predicate O.rel = O.lt,
goal O.trans
(* Sorted lists are correct association lists with unicity property. *)
let rec lemma increasing_unique_and_correct (o:order 'a)
(l:list (t 'a 'b)) : unit
requires { S.increasing o l }
ensures { correct o l }
ensures { unique o l }
variant { l }
= match l with Cons _ q -> increasing_unique_and_correct o q | _ -> () end
let lemma absent (o:order 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit
requires { correct_for o k }
requires { S.increasing o l }
requires { S.increasing o r }
requires { S.majorate o k l }
requires { S.minorate o k r }
ensures { model o (l++r) k = None }
= assert { S.precede o l r && not appear o k (l++r) &&
match model o (l++r) k with None -> true | _ -> false end }
let lemma present (o:order 'a) (k:key 'a) (l r:list (t 'a 'b))
(d:t 'a 'b) : unit
requires { correct_for o k }
requires { correct_for o (key d) }
requires { S.increasing o l }
requires { S.increasing o r }
requires { S.majorate o k l }
requires { S.minorate o k r }
requires { eq o k (key d) }
ensures { model o (l++Cons d r) k = Some d }
= assert { S.increasing o (l++Cons d r) }
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="4">
<prover
id="0"
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="1"
name="CVC4"
version="1.3"/>
<file
name="../association_list.mlw"
verified="true"
expanded="false">
<theory
name="Assoc"
locfile="../association_list.mlw"
loclnum="5" loccnumb="7" loccnume="12"
verified="true"
expanded="false">
<goal
name="WP_parameter model_occurence"
locfile="../association_list.mlw"
loclnum="43" loccnumb="16" loccnume="31"
expl="VC for model_occurence"
sum="45769d0afeebf6f4a3ba55e1301b497c"
proved="true"
expanded="false"
shape="CCfaNonetaSomewainfix @amodelV0V2V1qaappearV0V1V2ICfaNonetaSomewainfix @amodelV0V3V1qaappearV0V1V3Aacorrect_forV0V1AacorrectV0V3ACfaNilainfix =V4V3aConswVV2aConswVCfaNonetaSomewainfix @amodelV0V2V1qaappearV0V1V2wV2Iacorrect_forV0V1AacorrectV0V2F">
<label
name="why3:lemma"/>
<label
name="expl:VC for model_occurence"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter model_link"
locfile="../association_list.mlw"
loclnum="53" loccnumb="16" loccnume="26"
expl="VC for model_link"
sum="9739759d0868921977d8b3a1b49a57ce"
proved="true"
expanded="false"
shape="CCtaNonearelV0V1akeyV4aSomeVainfix @amodelV0V2V1ICtaNonearelV0V1akeyV5aSomeVainfix @amodelV0V3V1Aacorrect_forV0V1AacorrectV0V3ACfaNilainfix =V6V3aConswVV2aConswVCtaNonearelV0V1akeyV7aSomeVainfix @amodelV0V2V1wV2Iacorrect_forV0V1AacorrectV0V2F">
<label
name="why3:lemma"/>
<label
name="expl:VC for model_link"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="WP_parameter model_equal"
locfile="../association_list.mlw"
loclnum="62" loccnumb="16" loccnume="27"
expl="VC for model_equal"
sum="aa1254a320c83582e7fc29731c7fa832"
proved="true"
expanded="false"
shape="Cainfix =ainfix @amodelV0V3V1ainfix @amodelV0V3V2Iainfix =ainfix @amodelV0V4V1ainfix @amodelV0V4V2AarelV0V1V2Aacorrect_forV0V2Aacorrect_forV0V1AacorrectV0V4ACfaNilainfix =V5V4aConswVV3aConswVainfix =ainfix @amodelV0V3V1ainfix @amodelV0V3V2wV3IarelV0V1V2Aacorrect_forV0V2Aacorrect_forV0V1AacorrectV0V3F">
<label
name="why3:lemma"/>
<label
name="expl:VC for model_equal"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.20"/>
</proof>
</goal>
<goal
name="WP_parameter model_unique"
locfile="../association_list.mlw"
loclnum="73" loccnumb="16" loccnume="28"
expl="VC for model_unique"
sum="47dbff96bc3e568578fa58414a7c422b"
proved="true"
expanded="false"
shape="Cainfix =ainfix @amodelV0V2akeyV4aSomeV4IamemV4V2FIainfix =ainfix @amodelV0V3akeyV5aSomeV5IamemV5V3FAacorrect_forV0V1AauniqueV0V3AacorrectV0V3ACfaNilainfix =V6V3aConswVV2aConswVainfix =ainfix @amodelV0V2akeyV7aSomeV7IamemV7V2FwV2Iacorrect_forV0V1AauniqueV0V2AacorrectV0V2F">
<label
name="why3:lemma"/>
<label
name="expl:VC for model_unique"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
<theory
name="AssocSorted"
locfile="../association_list.mlw"
loclnum="86" loccnumb="7" loccnume="18"
verified="true"
expanded="false">
<goal
name="refl"
locfile="../relations_params.mlw"
loclnum="14" loccnumb="8" loccnume="12"
sum="1a8956218bada7ab4930cddaeeef3bec"
proved="true"
expanded="false"
shape="aeqV0V1V1Iacorrect_forV0V1F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="trans"
locfile="../relations_params.mlw"
loclnum="26" loccnumb="8" loccnume="13"
sum="a22194a9f5910222aa5a236bdfc99770"
proved="true"
expanded="false"
shape="aeqV0V1V3IaeqV0V2V3AaeqV0V1V2Iacorrect_forV0V3Aacorrect_forV0V2Aacorrect_forV0V1F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="symm"
locfile="../relations_params.mlw"
loclnum="33" loccnumb="8" loccnume="12"
sum="1a64b738c70a0907335259ac80c9199d"
proved="true"
expanded="false"
shape="aeqV0V2V1IaeqV0V1V2Iacorrect_forV0V2Aacorrect_forV0V1F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="trans"
locfile="../relations_params.mlw"
loclnum="26" loccnumb="8" loccnume="13"
sum="57cc4ca5b30f82016e2735ad84387f35"
proved="true"
expanded="false"
shape="altV0V1V3IaltV0V2V3AaltV0V1V2Iacorrect_forV0V3Aacorrect_forV0V2Aacorrect_forV0V1F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter increasing_unique_and_correct"
locfile="../association_list.mlw"
loclnum="112" loccnumb="16" loccnume="45"
expl="VC for increasing_unique_and_correct"
sum="a5b0cd3f3756f501c793764cd9dd80d5"
proved="true"
expanded="false"
shape="CauniqueV0V1AacorrectV0V1IauniqueV0V2AacorrectV0V2AaincreasingV0V2ACfaNilainfix =V3V2aConswVV1aConswVauniqueV0V1AacorrectV0V1wV1IaincreasingV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for increasing_unique_and_correct"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter absent"
locfile="../association_list.mlw"
loclnum="120" loccnumb="12" loccnume="18"
expl="VC for absent"
sum="54118473a904052020bb4488cfbde2e0"
proved="true"
expanded="false"
shape="ainfix =ainfix @amodelV0ainfix ++V2V3V1aNoneACtaNonefwainfix @amodelV0ainfix ++V2V3V1ANaappearV0V1ainfix ++V2V3AaprecedeV0V2V3IaminorateV0V1V3AamajorateV0V1V2AaincreasingV0V3AaincreasingV0V2Aacorrect_forV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for absent"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter absent.1"
locfile="../association_list.mlw"
loclnum="120" loccnumb="12" loccnume="18"
expl="1. assertion"
sum="de830a3390d1df6cab38826ff1b947a7"
proved="true"
expanded="false"
shape="assertionCtaNonefwainfix @amodelV0ainfix ++V2V3V1ANaappearV0V1ainfix ++V2V3AaprecedeV0V2V3IaminorateV0V1V3AamajorateV0V1V2AaincreasingV0V3AaincreasingV0V2Aacorrect_forV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for absent"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.15"/>
</proof>
</goal>
<goal
name="WP_parameter absent.2"
locfile="../association_list.mlw"
loclnum="120" loccnumb="12" loccnume="18"
expl="2. postcondition"
sum="ec0a38edf20083f1351bdac1fd06049a"
proved="true"
expanded="false"
shape="postconditionainfix =ainfix @amodelV0ainfix ++V2V3V1aNoneICtaNonefwainfix @amodelV0ainfix ++V2V3V1ANaappearV0V1ainfix ++V2V3AaprecedeV0V2V3IaminorateV0V1V3AamajorateV0V1V2AaincreasingV0V3AaincreasingV0V2Aacorrect_forV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for absent"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter present"
locfile="../association_list.mlw"
loclnum="130" loccnumb="12" loccnume="19"
expl="VC for present"
sum="704539429ba98492bc30fcb57c9dfb0d"
proved="true"
expanded="false"
shape="ainfix =ainfix @amodelV0ainfix ++V2aConsV4V3V1aSomeV4AaincreasingV0ainfix ++V2aConsV4V3IaeqV0V1akeyV4AaminorateV0V1V3AamajorateV0V1V2AaincreasingV0V3AaincreasingV0V2Aacorrect_forV0akeyV4Aacorrect_forV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for present"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter present.1"
locfile="../association_list.mlw"
loclnum="130" loccnumb="12" loccnume="19"
expl="1. assertion"
sum="5f188f15b8da6a38eafe87b0ec4b9f21"
proved="true"
expanded="false"
shape="assertionaincreasingV0ainfix ++V2aConsV4V3IaeqV0V1akeyV4AaminorateV0V1V3AamajorateV0V1V2AaincreasingV0V3AaincreasingV0V2Aacorrect_forV0akeyV4Aacorrect_forV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for present"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter present.1.1"
locfile="../association_list.mlw"
loclnum="130" loccnumb="12" loccnume="19"
expl="1. assertion"
sum="5f188f15b8da6a38eafe87b0ec4b9f21"
proved="true"
expanded="false"
shape="assertionaincreasingV0ainfix ++V2aConsV4V3IaeqV0V1akeyV4AaminorateV0V1V3AamajorateV0V1V2AaincreasingV0V3AaincreasingV0V2Aacorrect_forV0akeyV4Aacorrect_forV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for present"/>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.19"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter present.2"
locfile="../association_list.mlw"
loclnum="130" loccnumb="12" loccnume="19"
expl="2. postcondition"
sum="c6829da9d9da50fe740850f978d07502"
proved="true"
expanded="false"
shape="postconditionainfix =ainfix @amodelV0ainfix ++V2aConsV4V3V1aSomeV4IaincreasingV0ainfix ++V2aConsV4V3IaeqV0V1akeyV4AaminorateV0V1V3AamajorateV0V1V2AaincreasingV0V3AaincreasingV0V2Aacorrect_forV0akeyV4Aacorrect_forV0V1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for present"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.67"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
(* Technical reason: type must be declared outside for clones to work
properly. *)
theory ParamsTypes
use import int.Int
type view_base 'c 'd =
| VEmpty
| VNode 'c 'd 'c int
type m_base 'c =
| Empty
| Node (m_base 'c) 'c (m_base 'c) int
end
(* AVL parameters: a binary tree structure
(exact representation is unknown), + a positive balancing
constant. *)
module Params
use import int.Int
(* type for data stored in the nodes. *)
clone program_type.Type2 as Data
(* Abstract binary tree structure. *)
namespace Tree
use export ParamsTypes
type m 'a 'b = m_base (Data.m 'a 'b)
clone export program_type.Type2 with type m = m
type view 'a 'b = view_base (t 'a 'b) (Data.t 'a 'b)
(* Construction/pattern-matching over the tree. *)
val empty () : t 'a 'b
ensures { result.m = Empty }
ensures { c result }
val node (l:t 'a 'b) (d:Data.t 'a 'b) (r:t 'a 'b) (h:int) : t 'a 'b
requires { c l /\ Data.c d /\ c r }
ensures { result.m = Node l.m d.Data.m r.m h }
ensures { c result }
val view (t:t 'a 'b) : view 'a 'b
ensures { match result with
| VEmpty -> t.m = Empty
| VNode l d r h -> t.m = Node l.m d.Data.m r.m h /\
c l /\ Data.c d /\ c r
end }
end
(* Balancing constant for the tree. This will bound
the height difference between the subtrees at a node of
the avl. Larger constant mean deeper trees but less
balancing operations. *)
constant balancing : int
axiom balancing_positive : balancing > 0
end
(* AVL, modeled as a doubly-ended list + a non-negative height. *)
module AVL
use import int.Int
use import bool.Bool
use import list.Append
use import HighOrd
use import option.Option
use import ref.Ref
(* AVL Parameters. *)
clone import Params as P
(* The model of an avl is morally a list. *)
type l 'a 'b = list (Data.m 'a 'b)
(* Excepted that we also expose an integer (the height of the tree),
and an additional invariant on data. *)
type m 'a 'b = {
lis : l 'a 'b;
hgt : int;
inv : Data.m 'a 'b -> bool;
}
(* Shortcut. *)
function node_model (l:l 'a 'b) (d:Data.m 'a 'b) (r:l 'a 'b) : l 'a 'b =
l ++ Cons d r
(* list obtained from a tree by infix traversal. *)
function list_model (t:Tree.m 'a 'b) : l 'a 'b = match t with
| Tree.Empty -> Nil