Commit d17784c6 authored by Martin Clochard's avatar Martin Clochard
Browse files

AVL example with cached values from monoid.

parent 036bdfd7
(* Association lists. *)
(* Association with respect to an equivalence relation. *)
module Assoc
clone import key_type.KeyType as K
clone import relations.Equivalence as Eq with type t = key
use import list.List
use import list.Mem
use import list.Append
use import option.Option
use import HighOrd
predicate appear (k:key) (l:list (t 'a)) =
exists x. mem x l /\ Eq.rel k x.key
lemma appear_append : forall k:key,l r:list (t 'a).
appear k (l++r) <-> appear k l \/ appear k r
(* Unique occurence (a desirable property of an association list). *)
predicate unique (l:list (t 'a)) = match l with
| Nil -> true
| Cons x q -> not appear x.key q /\ unique q
end
(* functional update with equivalence classes. *)
function equiv_update (f:key -> 'b) (k:key) (b:'b) : key -> 'b =
\k2. if Eq.rel k k2 then b else f k2
function const_none : 'a -> option 'b = \x.None
(* functional model of an association list. *)
function model (l:list (t 'a)) : key -> option (t 'a) =
match l with
| Nil -> const_none
| Cons d q -> equiv_update (model q) d.key (Some d)
end
(* A key is bound iff it occurs in the association lists. *)
let rec lemma model_occurence (k:key) (l:list (t 'a)) : unit
ensures { appear k l <-> match model l k with None -> false
| Some _ -> true end }
ensures { not appear k l <-> model l k = None }
variant { l }
= match l with Cons _ q -> model_occurence k q | _ -> () end
(* A key is bound to a value with an equivalent key. *)
let rec lemma model_link (k:key) (l:list (t 'a)) : unit
ensures { match model l k with None -> true
| Some d -> Eq.rel k d.key end }
variant { l }
= match l with Cons _ q -> model_link k q | _ -> () end
(* Two equivalent keys are bound to the same value. *)
let rec lemma model_equal (k1 k2:key) (l:list (t 'a)) : unit
requires { Eq.rel k1 k2 }
ensures { model l k1 = model l k2 }
variant { l }
= match l with
| Cons _ q -> model_equal 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 (k:key) (l:list (t 'a)) : unit
requires { unique l }
ensures { forall d. mem d l -> model l d.key = Some d }
variant { l }
= match l with Cons _ q -> model_unique k q | _ -> () end
(* Singleton association list. *)
let lemma model_singleton (k:key) (d:t 'a) : unit
ensures { model (Cons d Nil) k = if rel k d.key then Some d else None }
= ()
(* Unique union of association list by concatenation. *)
let rec lemma model_concat (k:key) (l r:list (t 'a)) : unit
requires { unique (l++r) /\ unique l /\ unique r }
ensures { match model l k with None -> model (l++r) k = model r k
| s -> model (l++r) k = s end }
ensures { match model r k with None -> model (l++r) k = model l k
| s -> model (l++r) k = s end }
ensures { model (l++r) k = None <->
model l k = None /\ model r k = None }
ensures { model l k = None \/ model r k = None }
variant { l }
= match l with
| Nil -> ()
| Cons _ q -> model_concat k q r
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.Full as O with type t = key
clone export Assoc with type K.key = K.key,
type K.t = K.t,
function K.key = K.key,
predicate Eq.rel = O.eq,
(* Duplicates, there is no need to keep them as lemma. *)
goal Eq.Trans,
goal Eq.Refl,
goal Eq.Symm
clone sorted.Increasing as S with type K.key = K.key,
type K.t = K.t,
function K.key = K.key,
predicate O.rel = O.lt,
goal O.Trans
(* Sorted lists are association lists with unicity property. *)
let rec lemma increasing_unique (l:list (t 'a)) : unit
requires { S.increasing l }
ensures { unique l }
variant { l }
= match l with Cons _ q -> increasing_unique q | _ -> () end
let lemma model_cut (k:key) (l r:list (t 'a)) : unit
requires { S.increasing r }
requires { S.increasing l }
requires { S.majorate k l }
requires { S.minorate k r }
ensures { forall k2. eq k k2 -> model (l++r) k2 = None }
ensures { forall k2. lt k k2 -> model (l++r) k2 = model r k2 }
ensures { forall k2. le k2 k -> model r k2 = None }
ensures { forall k2. lt k2 k -> model (l++r) k2 = model l k2 }
ensures { forall k2. le k k2 -> model l k2 = None }
= assert { S.increasing (l++r) };
assert { forall k2. lt k k2 -> model (l++r) k2 <> model r k2 ->
match model r k2 with
| None -> match model l k2 with
| None -> false
| Some d -> lt d.key k && false
end && false
| _ -> false
end && false };
assert { forall k2. lt k2 k -> model (l++r) k2 <> model l k2 ->
match model l k2 with
| None -> match model r k2 with
| None -> false
| Some d -> lt k d.key && false
end && false
| _ -> false
end && false };
assert { forall k2. eq k k2 -> model (l++r) k2 <> None ->
(not appear k2 l /\ not appear k2 r) && false }
let lemma model_split (d:t 'a) (l r:list (t 'a)) : unit
requires { S.increasing l }
requires { S.increasing r }
requires { S.majorate d.key l }
requires { S.minorate d.key r }
ensures { forall k2. eq d.key k2 -> model (l++Cons d r) k2 = Some d }
ensures { forall k2. lt d.key k2 -> model (l++Cons d r) k2 = model r k2 }
ensures { forall k2. le k2 d.key -> model r k2 = None }
ensures { forall k2. lt k2 d.key -> model (l++Cons d r) k2 = model l k2 }
ensures { forall k2. le d.key k2 -> model l k2 = None }
= ()
end
This diff is collapsed.
This diff is collapsed.
(* Type with a key. Intended to factor elements/bindings representations
in sets/map-like structures, so it is essentially intended for two cases:
- t 'a = key
- t 'a = key * 'a *)
theory KeyType
type t 'a
type key
function key (t 'a) : key
end
module ProgramKeyType
use import program_type.TypeParams
clone program_type.Type0 as K
clone program_type.Type1 as D
clone export KeyType with type t = D.m, type key = K.m
val get_key (ghost p:type_params 'a 'b) (t:D.t 'a 'b) : K.t
requires { p.D.mp.inv t }
ensures { K.c result }
ensures { key (p.D.mp.mdl t) = result.K.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="4">
<file
name="../key_type.mlw"
verified="true"
expanded="false">
<theory
name="KeyType"
locfile="../key_type.mlw"
loclnum="6" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
</theory>
<theory
name="ProgramKeyType"
locfile="../key_type.mlw"
loclnum="14" loccnumb="7" loccnume="21"
verified="true"
expanded="false">
</theory>
</file>
</why3session>
This diff is collapsed.
This diff is collapsed.
module Monoid
type t
constant zero : t
function add (a b:t) : t
axiom assoc : forall a b c:t. add a (add b c) = add (add a b) c
axiom neutral : forall x:t. add x zero = x = add zero x
end
module MonoidList
use import list.Append
use import HighOrd
clone import Monoid as M
(* Because definitions cannot be replicated via cloning. *)
function sum (f:'a -> t) (l:list 'a) : t
axiom sum_def_nil : forall f:'a -> t. sum f Nil = zero
axiom sum_def_cons : forall f:'a -> t,x,q.
sum f (Cons x q) = add (f x) (sum f q)
let rec lemma sum_append (f:'a -> t) (l r:list 'a) : unit
ensures { sum f (l ++ r) = add (sum f l) (sum f r) }
variant { l }
= match l with Cons _ q -> sum_append f q r | _ -> () end
end
module MonoidListDef
use import list.List
use import HighOrd
namespace M
type t
constant zero : t
function add (a b:t) : t
end
function sum (f:'a -> M.t) (l:list 'a) : M.t = match l with
| Nil -> M.zero
| Cons x q -> M.add (f x) (sum f q)
end
clone export MonoidList with type M.t = M.t,constant M.zero = M.zero,
function M.add = M.add,function sum = sum,
goal sum_def_nil,goal sum_def_cons
end
module ComputableMonoid
use import program_type.TypeParams
clone export program_type.Type0
clone export Monoid with type t = m
val zero () : t
ensures { c result /\ result.m = zero }
val add (a b:t) : t
requires { c a /\ c b }
ensures { c result /\ result.m = add a.m b.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="4">
<prover
id="0"
name="Alt-Ergo"
version="0.95.2"/>
<file
name="../monoid.mlw"
verified="true"
expanded="true">
<theory
name="Monoid"
locfile="../monoid.mlw"
loclnum="2" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
</theory>
<theory
name="MonoidList"
locfile="../monoid.mlw"
loclnum="14" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter sum_append"
locfile="../monoid.mlw"
loclnum="26" loccnumb="16" loccnume="26"
expl="VC for sum_append"
sum="93f3fef7f24026ff7ffc85f1eeab1ce1"
proved="true"
expanded="true"
shape="Cainfix =asumV0ainfix ++V1V2aaddasumV0V1asumV0V2Iainfix =asumV0ainfix ++V3V2aaddasumV0V3asumV0V2ACfaNilainfix =V4V3aConswVV1aConswVainfix =asumV0ainfix ++V1V2aaddasumV0V1asumV0V2wV1F">
<label
name="why3:lemma"/>
<label
name="expl:VC for sum_append"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
<theory
name="MonoidListDef"
locfile="../monoid.mlw"
loclnum="33" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
<goal
name="sum_def_nil"
locfile="../monoid.mlw"
loclnum="22" loccnumb="8" loccnume="19"
sum="1fabfcb4f1d5fd8cff9c9422b1af6f6e"
proved="true"
expanded="true"
shape="ainfix =asumV0aNilazeroF">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="sum_def_cons"
locfile="../monoid.mlw"
loclnum="23" loccnumb="8" loccnume="20"
sum="74a8baa5028da06c811d858ba41c263f"
proved="true"
expanded="true"
shape="ainfix =asumV0aConsV1V2aaddainfix @V0V1asumV0V2F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory
name="ComputableMonoid"
locfile="../monoid.mlw"
loclnum="52" loccnumb="7" loccnume="23"
verified="true"
expanded="true">
</theory>
</file>
</why3session>
(* Full preorder theory,
containing lt and eq as well. *)
theory Full
type t
predicate le t t
clone export relations.PreOrder with type t = t, predicate rel = le
predicate eq t t
axiom eq_def : forall x y. eq x y <-> le x y /\ le y x
predicate lt t t
axiom lt_def : forall x y. lt x y <-> le x y /\ not le y x
clone relations.Equivalence as Eq with type t = t,
predicate rel = eq, lemma Trans, lemma Refl, lemma Symm
clone relations.PartialStrictOrder as Lt with type t = t,
predicate rel = lt, lemma Trans, lemma Asymm
end
theory TotalFull
clone export Full
clone export relations.Total with type t = t, predicate rel = le
clone relations.Total as Lt with type t = t,
predicate rel = le, goal Total
lemma lt_def2 : forall x y. lt x y <-> not le y x
end
(* Total preorder + corresponding program types and computable comparison. *)
module Computable
use import int.Int
clone program_type.Type0 as T
clone export TotalFull with type t = T.m
(* Comparison is computable. *)
val compare (x y:T.t) : int
requires { T.c x /\ T.c y }
ensures { let xm = x.T.m in let ym = y.T.m in
(result > 0 <-> lt ym xm) /\
(result < 0 <-> lt xm ym) /\
(result = 0 <-> eq xm ym) }
end
This diff is collapsed.
module TypeParams
use import HighOrd
(* Additional information for parametric programs:
'a represent the program type (the effective datatype),
'b represent its logical model (the reasoning datatype),
which may be different from the effective datatype.
Also, one need the representation invariant over the 'a datatype.
inv is the representation invariant of 'a,
mdl the function mapping the program representation to its logical model.
*)
type type_params 'a 'b = {
inv : 'a -> bool;
mdl : 'a -> 'b;
}
(* For purely logical types. *)
constant default_params : type_params 'a 'a
axiom default_params_def : (default_params:type_params 'a 'a) = {
inv = \n. true;
mdl = \x. x;
}
end
module Type0
use import TypeParams
(* Program version of the type. *)
type t
(* Its logical model. *)
type m
(* Type invariant (c for correct). *)
predicate c t
(* get logical model (m for model). *)
function m t : m
(* Parametric information (for use in polymorphic code). *)
constant mp : type_params t m = { inv = (\t. c t); mdl = (\t. m t) }
end
(* Variants with different number of type variables. *)
module Type1
use import TypeParams
(* Need two types variables to represent both the program and logic worlds. *)
type t 'a 'b
type m 'b
(* Parametric model and invariants. *)
function mp (type_params 'a 'b) : type_params (t 'a 'b) (m 'b)
end
(* Variant for a type storing explicitly its parameters
(typically in ghost fields). *)
module Type1Prm
use import TypeParams
type t 'a 'b
type m 'b
predicate c (t 'a 'b)
function m (t 'a 'b) : m 'b
function prm (t 'a 'b) : type_params 'a 'b
function mp (p:type_params 'a 'b) : type_params (t 'a 'b) (m 'b) =
{ inv = (\t. c t /\ prm t = p);
mdl = (\t. m t) }
end
module Type2
use import TypeParams
type t 'a 'b 'c 'd
type m 'b 'd
function mp (type_params 'a 'b)
(type_params 'c 'd) : type_params (t 'a 'b 'c 'd) (m 'b 'd)
end
module Type2Prm
use import TypeParams
type t 'a 'b 'c 'd
type m 'b 'd
predicate c (t 'a 'b 'c 'd)
function m (t 'a 'b 'c 'd) : m 'b 'd
function prm1 (t 'a 'b 'c 'd) : type_params 'a 'b
function prm2 (t 'a 'b 'c 'd) : type_params 'c 'd
function mp (p1:type_params 'a 'b) (p2:type_params 'c 'd) :
type_params (t 'a 'b 'c 'd) (m 'b 'd) =
{ inv = (\t. c t /\ prm1 t = p1 /\ prm2 t = p2);
mdl = (\t. m t) }
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">
<file
name="../program_type.mlw"
verified="true"
expanded="true">
<theory
name="TypeParams"
locfile="../type_params.mlw"
loclnum="2" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
</theory>
</file>
</why3session>
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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