Commit bab7500c authored by Andrei Paskevich's avatar Andrei Paskevich

Merge remote-tracking branch 'origin/clone_val'

parents 836d876d 68d0207b
......@@ -9,17 +9,19 @@ module Assoc
use import list.List
use import list.Mem
use import list.Append
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)
lemma appear_append : forall p:param 'a,k:key 'a,l r:list (t 'a 'b).
appear p k (l++r) <-> appear p k l \/ appear p k r
(* 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
predicate correct (p:param 'a) (l:list (t 'a 'b)) =
forall x. mem x l -> let kx = key x in correct_for p kx
(* Unique occurence (a desirable property of an association list). *)
predicate unique (p:param 'a) (l:list (t 'a 'b)) = match l with
......@@ -32,10 +34,12 @@ module Assoc
(k:key 'a) (b:'b) : key 'a -> 'b = \k2.
if Eq.rel p k k2 then b else f k2
function const_none : 'a -> option 'b = \x.None
(* 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
| Nil -> const_none
| Cons d q -> param_update p (model p q) (key d) (Some d)
end
......@@ -46,6 +50,7 @@ module Assoc
requires { correct_for p k }
ensures { appear p k l <-> match model p l k with None -> false
| Some _ -> true end }
ensures { not appear p k l <-> model p l k = None }
variant { l }
= match l with Cons _ q -> model_occurence p k q | _ -> () end
......@@ -66,7 +71,11 @@ module Assoc
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
= match l with
| Cons x q -> assert { correct_for p x.key };
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. *)
......@@ -78,6 +87,36 @@ module Assoc
variant { l }
= match l with Cons _ q -> model_unique p k q | _ -> () end
(* Singleton association list. *)
let lemma model_singleton (p:param 'a) (k:key 'a) (d:t 'a 'b) : unit
requires { correct_for p d.key }
requires { correct_for p k }
ensures { model p (Cons d Nil) k = if rel p k d.key
then Some d
else None }
= ()
(* Unique union of association list by concatenation. *)
let rec lemma model_concat (p:param 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit
requires { correct p (l++r) /\ correct p l /\ correct p r }
requires { unique p (l++r) /\ unique p l /\ unique p r }
requires { correct_for p k }
ensures { match model p l k with None -> model p (l++r) k = model p r k
| s -> model p (l++r) k = s end }
ensures { match model p r k with None -> model p (l++r) k = model p l k
| s -> model p (l++r) k = s end }
ensures { model p (l++r) k = None <->
model p l k = None /\ model p r k = None }
ensures { model p l k = None \/ model p r k = None }
variant { l }
= match l with
| Nil -> ()
| Cons d q -> assert { rel p d.key k -> model p r k <> None ->
match model p r k with None -> false | _ -> not appear p k r && false end
&& false };
model_concat p k q r
end
end
......@@ -92,17 +131,15 @@ module AssocSorted
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*)
clone export Assoc with namespace K = K,
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. *)
(* 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 namespace K = K,
(*namespace O = O.Lt*)
type O.param = O.order,
predicate O.correct_for = O.correct_for,
predicate O.rel = O.lt,
......@@ -117,27 +154,57 @@ module AssocSorted
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
let lemma model_cut (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.increasing o l }
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) }
ensures { forall k2. correct_for o k2 /\ eq o k k2 ->
model o (l++r) k2 = None }
ensures { forall k2. correct_for o k2 /\ lt o k k2 ->
model o (l++r) k2 = model o r k2 }
ensures { forall k2. correct_for o k2 /\ le o k2 k ->
model o r k2 = None }
ensures { forall k2. correct_for o k2 /\ lt o k2 k ->
model o (l++r) k2 = model o l k2 }
ensures { forall k2. correct_for o k2 /\ le o k k2 ->
model o l k2 = None }
= assert { S.increasing o (l++r) };
assert { forall k2. correct_for o k2 /\ lt o k k2 ->
model o (l++r) k2 <> model o r k2 -> match model o r k2 with
| None -> match model o l k2 with
| None -> false
| Some d -> lt o d.key k && false
end && false
| _ -> false
end && false };
assert { forall k2. correct_for o k2 /\ lt o k2 k ->
model o (l++r) k2 <> model o l k2 -> match model o l k2 with
| None -> match model o r k2 with
| None -> false
| Some d -> lt o k d.key && false
end && false
| _ -> false
end && false }
let lemma model_split (o:order 'a) (d:t 'a 'b) (l r:list (t 'a 'b)) : unit
requires { correct_for o d.key }
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) }
requires { S.majorate o d.key l }
requires { S.minorate o d.key r }
ensures { forall k2. correct_for o k2 /\ eq o d.key k2 ->
model o (l++Cons d r) k2 = Some d }
ensures { forall k2. correct_for o k2 /\ lt o d.key k2 ->
model o (l++Cons d r) k2 = model o r k2 }
ensures { forall k2. correct_for o k2 /\ le o k2 d.key ->
model o r k2 = None }
ensures { forall k2. correct_for o k2 /\ lt o k2 d.key ->
model o (l++Cons d r) k2 = model o l k2 }
ensures { forall k2. correct_for o k2 /\ le o d.key k2 ->
model o l k2 = None }
= ()
end
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
(* Type with a key. Intended to factor elements/bindings representations
in sets/map-like structures.
Typical instantiation:
- Set elements, t 'a 'b = key 'a, get_key = id:
the only information one can retrieve
from a key is presence.
- Map bindings, t 'a 'b = (key 'a,value 'b),get_key = fst:
one can also retrieve a value from a present binding. *)
in sets/map-like structures, so it is essentially intended for two cases:
- t 'a 'b = key 'a
- t 'a 'b = key 'a * 'b *)
theory KeyType
type t 'a 'b
......@@ -15,16 +11,21 @@ theory KeyType
end
(* program version. *)
module ProgramKeyType
clone export program_type.Type2
clone program_type.Type1 as Key
function key_m (m 'a 'b) : Key.m 'a
val key (x:t 'a 'b) : Key.t 'a
requires { c x }
ensures { Key.c result }
ensures { x.m.key_m = result.Key.m }
use import program_type.TypeParams
clone program_type.Type1 as K
clone program_type.Type2 as D
clone export KeyType with type t = D.m, type key = K.m
val get_key (ghost p1:type_params 'a 'b)
(ghost p2:type_params 'c 'd)
(t:D.t 'a 'b 'c 'd) : K.t 'a 'b
requires { (D.make_params p1 p2).inv t }
ensures { (K.make_params p1).inv result }
ensures { key ((D.make_params p1 p2).mdl t) =
(K.make_params p1).mdl result }
end
......@@ -4,20 +4,20 @@
<file
name="../key_type.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="KeyType"
locfile="../key_type.mlw"
loclnum="3" loccnumb="7" loccnume="14"
loclnum="6" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
expanded="false">
</theory>
<theory
name="ProgramKeyType"
locfile="../key_type.mlw"
loclnum="12" loccnumb="7" loccnume="21"
loclnum="14" loccnumb="7" loccnume="21"
verified="true"
expanded="true">
expanded="false">
</theory>
</file>
</why3session>
This diff is collapsed.
This diff is collapsed.
(* 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.upper_bound k l }
requires { S.lower_bound 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.upper_bound d.key l }
requires { S.lower_bound 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 op (a b:t) : t
axiom assoc : forall a b c:t. op a (op b c) = op (op a b) c
axiom neutral : forall x:t. op x zero = x = op 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) = op (f x) (sum f q)
let rec lemma sum_append (f:'a -> t) (l r:list 'a) : unit
ensures { sum f (l ++ r) = op (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 op (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.op (f x) (sum f q)
end
clone export MonoidList with type M.t = M.t,constant M.zero = M.zero,
function M.op = M.op,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 op (a b:t) : t
requires { c a /\ c b }
ensures { c result /\ result.m = op 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