 ### examples/avl: portage vers le nouveau système

parent d98661f6
 (** {1 Facts about association lists} Author: Martin Clochard *) (** {2 Association with respect to an equivalence relation} *) module Assoc (** Abstract type for objects identified by keys. *) clone import key_type.KeyType as K (** Abstract equivalence relation. *) 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 (** Existence of an element identified by key [k] in list [l]. *) 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 of every key *) 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 = fun k2 -> if Eq.rel k k2 then b else f k2 function const_none : 'a -> option 'b = fun _ -> None (** Association list viewed as a partial mapping *) 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. Equivalently, [appear] describe the domain of the partial mapping. *) let rec lemma model_domain (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_domain k q | _ -> () end (** A key is bound to a value with an equivalent key. *) let rec lemma model_key (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_key k q | _ -> () end (** Congruence lemma. *) let rec lemma model_congruence (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_congruence 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 } = () (** Link between disjoint concatenation and disjoint union of partial mappings. *) 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 (** {2 Sorted association lists} *) module AssocSorted use import list.List use import list.Append use import list.Mem use import option.Option (** It is an instance of association lists. *) 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, goal Eq.Trans, goal Eq.Refl, goal Eq.Symm (** Consider sorted (increasing) lists. *) 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 have 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 (** Description of the partial mapping corresponding to the concatenation of increasing lists separated by a known key in the middle. *) 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 } (** Description of the partial mapping corresponding to a list split around a midpoint. *) 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

File deleted
This diff is collapsed.
This diff is collapsed.
No preview for this file type
 ... ... @@ -8,21 +8,12 @@ representations for sets/map-like structures, as it can be used both for elements and key-value pairs. *) (** {2 Logical type with key} *) theory KeyType (** {2 Keyed type.} *) module KeyType type t 'a type key function key (t 'a) : key end (** {2 Program type with key} *) module ProgramKeyType clone export KeyType val get_key (t:t 'a) : key ensures { key t = result } val function key (t:t 'a) : key end
 ... ... @@ -5,7 +5,5 @@
 ... ... @@ -23,43 +23,47 @@ end (** {2 Abstract monoid with aggregation} *) module MonoidSum use import list.List use import list.Append use import seq.Seq clone import Monoid as M (** Axiomatized definition of the monoidal aggregation of elements obtained from a list: using infix notation for the monoid law, [sum f [a_1;a_2;...;a_n]] is [a_1 op a_2 ... op a_n]. This axiomatization must be kept until the monoid is instantiated *) 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) (** Consequence of associativity *) 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 function agg (f:'a -> t) (s:seq 'a) : t axiom agg_empty : forall f:'a -> t. agg f empty = zero axiom agg_sing : forall f,s:seq 'a. length s = 1 -> agg f s = f s axiom agg_cat : forall f,s1 s2:seq 'a. agg f (s1 ++ s2) = op (agg f s1) (agg f s2) end (** {2 Definition of aggregation} *) (** {2 Definition of aggregation (refinement of MonoidSum} *) module MonoidSumDef use import list.List scope 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 MonoidSum 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 use import seq.Seq use import seq.FreeMonoid (* TODO: do that refinement correctly ! *) clone import Monoid as M let rec ghost function agg (f:'a -> t) (s:seq 'a) : M.t variant { length s } = if length s = 0 then zero else op (f s) (agg f s[1 ..]) lemma agg_sing_core : forall s:seq 'a. length s = 1 -> s[1 ..] == empty let rec lemma agg_cat (f:'a -> t) (s1 s2:seq 'a) ensures { agg f (s1++s2) = op (agg f s1) (agg f s2) } variant { length s1 } = if length s1 <> 0 then let s3 = s1[1 ..] in agg_cat f s3 s2 clone MonoidSum as MS with type M.t = M.t, constant M.zero = M.zero, function M.op = M.op, goal M.assoc, goal M.neutral, function agg = agg, goal agg_empty, goal agg_sing, goal agg_cat end ... ...
 ... ... @@ -2,21 +2,37 @@ ... ...
No preview for this file type
 ... ... @@ -44,8 +44,9 @@ module Computable (** Comparison is computable. *) val compare (x y:t) : int ensures { (result > 0 <-> lt y x) /\ (result < 0 <-> lt x y) /\ (result = 0 <-> eq x y) } ensures { result > 0 <-> lt y x } ensures { result < 0 <-> lt x y } ensures { result = 0 <-> eq x y } end
 ... ... @@ -2,31 +2,31 @@ ... ...
No preview for this file type
This diff is collapsed.
This diff is collapsed.
No preview for this file type
This diff is collapsed.
This diff is collapsed.
No preview for this file type
 (** {1 Sorted list with respect to a transitive relation over keys} Author: Martin Clochard *) module Increasing use import list.List use import list.Mem use import list.Append (** Abstract structure carrying keys. *) clone import key_type.KeyType as K (** Abstract transitive relation. *) clone import relations.Transitive as O with type t = key (** Strict bounds over lists. *) predicate lower_bound (x:key) (l:list (t 'a)) = (forall y. mem y l -> rel x y.key) predicate upper_bound (x:key) (l:list (t 'a)) = (forall y. mem y l -> rel y.key x) (** A list [l1] precede another list [l2] if every element of [l1] is before every element of [l2]. *) predicate precede (l1 l2:list (t 'a)) = (forall x y. mem x l1 /\ mem y l2 -> rel x.key y.key) lemma smaller_lower_bound : forall kdown kup,l:list (t 'a). lower_bound kup l /\ rel kdown kup -> lower_bound kdown l lemma bigger_upper_bound : forall kdown kup,l:list (t 'a). upper_bound kdown l /\ rel kdown kup -> upper_bound kup l (** Define increasing lists. *) predicate increasing (l:list (K.t 'a)) = match l with | Nil -> true | Cons x q -> lower_bound x.K.key q /\ increasing q end (** Conditions for a list concatenation to be increasing. *) let rec lemma increasing_precede (l r:list (K.t 'a)) ensures { increasing (l++r) <-> increasing l /\ increasing r /\ precede l r } variant { l } = match l with | Nil -> () | Cons _ q -> increasing_precede q r end (** Variant of the above condition, with a midpoint. *) let lemma increasing_midpoint (l:list (K.t 'a)) (x:K.t 'a) (r:list (K.t 'a)) : unit ensures { let kx = K.key x in increasing (l++Cons x r) <-> increasing l /\ increasing r /\ lower_bound kx r /\ upper_bound kx l } = () (** Symetric definition of increasing lists, starting at the end. *) let lemma increasing_snoc (l:list (K.t 'a)) (x:K.t 'a) : unit ensures { let kx = K.key x in increasing (l++Cons x Nil) <-> increasing l /\ upper_bound kx l } = () end