Commit 5432d834 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into claude

parents d35cf9c3 e0abc171
......@@ -120,6 +120,10 @@ let test () =
interpret_0 p4)
constant v3 : int = eval_0 p3
goal eval_p3 : v3 = 1
end
......@@ -227,13 +231,7 @@ function size_e (e:expr) : int =
| Sub e1 e2 -> 3 + size_e e1 + size_e e2
end
let rec lemma size_e_pos (e:expr) : unit
variant { e }
ensures { size_e e >= 1 }
= match e with
| Cte _ -> ()
| Sub e1 e2 -> size_e_pos e1; size_e_pos e2
end
lemma size_e_pos: forall e: expr. size_e e >= 1
function size_c (c:cont) : int =
match c with
......@@ -242,14 +240,7 @@ function size_c (c:cont) : int =
| A2 _ k -> 1 + size_c k
end
let rec lemma size_c_pos (c:cont) : unit
variant { c }
ensures { size_c c >= 0 }
= match c with
| I -> ()
| A1 _ k -> size_c_pos k
| A2 _ k -> size_c_pos k
end
lemma size_c_pos: forall c: cont. size_c c >= 0
(** WhyML programs (declared with "let" instead of "function"),
mutually recursive, resulting from de-functionalization *)
......@@ -290,7 +281,7 @@ let test () =
end
(** {2 Defunctionalization with an alebraic variant} *)
(** {2 Defunctionalization with an algebraic variant} *)
module Defunctionalization2
......@@ -512,15 +503,8 @@ function eval_1 (e:expr) (k:value -> 'a) : 'a =
function interpret_1 (p : prog) : value = eval_1 p (\ n. n)
let rec lemma cps_correct_expr (e:expr) : unit
variant { e }
ensures { forall k:value -> 'a. eval_1 e k = k (eval_0 e) }
= match e with
| Cte _ -> ()
| Sub e1 e2 ->
cps_correct_expr e1;
cps_correct_expr e2
end
lemma cps_correct_expr:
forall e: expr. forall k:value -> 'a. eval_1 e k = k (eval_0 e)
lemma cps_correct: forall p. interpret_1 p = interpret_0 p
......@@ -694,13 +678,7 @@ function size_e (e:expr) : int =
| Sub e1 e2 -> 3 + size_e e1 + size_e e2
end
let rec lemma size_e_pos (e:expr) : unit
variant { e }
ensures { size_e e >= 1 }
= match e with
| Cte _ -> ()
| Sub e1 e2 -> size_e_pos e1; size_e_pos e2
end
lemma size_e_pos: forall e: expr. size_e e >= 1
use Defunctionalization
......@@ -711,14 +689,7 @@ function size_c (c:cont) : int =
| B _ k -> 1 + size_c k
end
let rec lemma size_c_pos (c:cont) : unit
variant { c }
ensures { size_c c >= 0 }
= match c with
| I -> ()
| A _ k -> size_c_pos k
| B _ k -> size_c_pos k
end
lemma size_c_pos: forall c: cont. size_c c >= 0
let rec continue_4 (c:cont) (v:int) : value
requires { v >= 0 }
......@@ -931,15 +902,7 @@ function size_c (c:context) : int =
| Right _ c -> 1 + size_c c
end
let rec lemma size_c_pos (c:context) : unit
variant { c }
ensures { size_c c >= 0 }
= match c with
| Empty -> ()
| Left c _ -> size_c_pos c
| Right _ c -> size_c_pos c
end
lemma size_c_pos: forall c: context. size_c c >= 0
let rec decompose_term (e:expr) (c:context) : (context, expr)
......@@ -1154,14 +1117,7 @@ function size_c (c:context) : int =
| Right _ c -> 1 + size_c c
end
let rec lemma size_c_pos (c:context) : unit
variant { c }
ensures { size_c c >= 0 }
= match c with
| Empty -> ()
| Left c _ -> size_c_pos c
| Right _ c -> size_c_pos c
end
lemma size_c_pos: forall c: context. size_c c >= 0
function recompose (c:context) (e:expr) : expr =
match c with
......
......@@ -475,7 +475,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.36"/>
<result status="valid" time="0.22"/>
</proof>
<proof
prover="1"
......@@ -782,127 +782,12 @@
<goal
name="WP_parameter go"
locfile="../euler001.mlw"
<<<<<<< HEAD
loclnum="193" loccnumb="6" loccnume="8"
expl="VC for go"
sum="0ac8af78cda25414bc3f614bbe49b1cf"
proved="true"
expanded="false"
shape="ainfix =V12ainfix +V0c1Iainfix =V15aConsareverseV11V3Aainfix =V12ainfix +V0c1Aainfix =V14aNilAainfix =V13c0FIainfix =V11aConsaPrCharamk charc32V9Aainfix =V10ainfix +V8c1FAainfix &lt;=c32c255Aainfix &lt;=c0c32Iainfix =V9aConsaPrCharamk charc58V7Aainfix =V8ainfix +V6c1FAainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FAainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FAainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter go.1"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="1. precondition"
sum="f4b435e3c7c416c20c0ceacb2df6b3c7"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter go.2"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="2. precondition"
sum="abd8cc3f32089b628b51946de8e1f545"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter go.3"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="3. precondition"
sum="52fac0728ac3d37e1cf005143aeda71d"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FIainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter go.4"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="4. precondition"
sum="b862795097c52804b1f9c8df726d5eb4"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c32c255Aainfix &lt;=c0c32Iainfix =V9aConsaPrCharamk charc58V7Aainfix =V8ainfix +V6c1FIainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FIainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter go.5"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="5. postcondition"
sum="ddceb58388c30c795f01682eeffde5dc"
proved="true"
expanded="false"
shape="postconditionainfix =V12ainfix +V0c1Iainfix =V15aConsareverseV11V3Aainfix =V12ainfix +V0c1Aainfix =V14aNilAainfix =V13c0FIainfix =V11aConsaPrCharamk charc32V9Aainfix =V10ainfix +V8c1FIainfix &lt;=c32c255Aainfix &lt;=c0c32Iainfix =V9aConsaPrCharamk charc58V7Aainfix =V8ainfix +V6c1FIainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FIainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
=======
loclnum="192" loccnumb="6" loccnume="8"
expl="VC for go"
sum="2eb916ae0bbffb9f85abd4e316b2b2c2"
proved="true"
expanded="false"
shape="ainfix &lt;=c32c255Aainfix &lt;=c0c32Aainfix &lt;=c58c255Aainfix &lt;=c0c58Aainfix &lt;=c79c255Aainfix &lt;=c0c79Aainfix &lt;=c71c255Aainfix &lt;=c0c71">
<label
name="expl:VC for go"/>
<proof
......@@ -913,7 +798,6 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
>>>>>>> master
</goal>
</theory>
</file>
......
......@@ -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 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.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -344,6 +344,7 @@ subst:
| CONSTANT qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
| VAL qualid EQUAL qualid { CSvsym (floc (), $2, $4) }
| LEMMA qualid { CSlemma (floc (), $2) }
| GOAL qualid { CSgoal (floc (), $2) }
;
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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