diff --git a/.DS_Store b/.DS_Store
new file mode 100644
index 0000000000000000000000000000000000000000..90bd44924b79ec5d54f3687165c3746c4a239273
Binary files /dev/null and b/.DS_Store differ
diff --git a/hoare/hoare_logic.mlw b/hoare/hoare_logic.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..fc3f515d3d872f19f6ca1a9e5acb113fc44e27ec
--- /dev/null
+++ b/hoare/hoare_logic.mlw
@@ -0,0 +1,410 @@
+module Sum
+
+ use int.Int
+ use ref.Ref
+
+ inductive sum int int =
+ | sum0 : sum 0 0
+ | sum1 : forall n m. sum n m -> sum (n + 1) (n + 1 + m)
+
+ goal s0: sum 0 0
+ goal s1: sum 1 (0 + 1)
+ goal s2: sum 2 (0 + 1 + 2)
+ goal s3: sum 3 (0 + 1 + 2 + 3)
+
+ function sumf int : int
+ axiom sumf_ax : forall a s. 0 <= a -> sum a s <-> s = sumf a
+ lemma sumf_lem: forall a s. 0 <= a -> s = sumf a -> sum a s
+
+ goal f0: sumf 0 = 0
+ goal f1: sumf 1 = 0 + 1
+ goal f2: sumf 2 = 0 + 1 + 2
+ goal f3: sumf 3 = 0 + 1 + 2 + 3
+
+ let rec sum_whyML_rec (n : int) : int
+ requires { 0 <= n }
+ variant { n }
+ ensures { sum n result }
+ ensures { result = sumf n } (* <- and/or alternatively *)
+ =
+ match n = 0 with
+ | True -> 0
+ | _ -> sum_whyML_rec (n - 1) + n
+ end
+
+ let sum_whyML (n : int) : int
+ requires { 0 <= n }
+ ensures { sum n result }
+ ensures { result = sumf n } (* <- and/or alternatively *)
+ =
+ let a = ref 0 in
+ let b = ref 0 in
+ while !a <= n - 1 do variant { n - !a }
+ invariant { 0 <= !a <= n /\ sum !a !b }
+ invariant { 0 <= !a <= n /\ !b = sumf !a } (* <- and/or alternatively *)
+ a := !a + 1;
+ b := !b + !a;
+ done;
+ !b
+
+ let ml0 () = let s = sum_whyML 0 in assert { s = 0 }; ()
+ let ml1 () = let s = sum_whyML 1 in assert { s = 1 }; ()
+ let ml2 () = let s = sum_whyML 2 in assert { s = 3 }; ()
+ let ml3 () = let s = sum_whyML 3 in assert { s = 6 }; ()
+
+
+end
+
+module Assignment
+
+ use int.Int
+
+ let f (x : int) : int
+ requires { 10 < x < 43 }
+ = x
+
+ let g (x : int) : int
+ (* requires { your code here } *)
+ = let x = x + 1 in
+ f x
+end
+
+module AssignmentRef
+
+ use int.Int
+ use ref.Ref
+
+ let f (x : ref int) : ref int
+ requires { 10 < !x < 43 }
+ = x
+
+ let g (x : ref int) : ref int
+ (* requires { your code here } *)
+ = x := !x + 1;
+ f x
+end
+
+module SequenceRef
+
+ use int.Int
+ use ref.Ref
+
+ let seq (x : ref int) : ref int
+ (* requires { your code here } *)
+ ensures { !result = 43 }
+ =
+ let y = ref 0 in
+ let z = ref 0 in
+ y := !x + 1;
+ z := !y;
+ z
+end
+
+module WhileRef
+
+ use int.Int
+ use ref.Ref
+
+ let loop (x: ref int) : ref int
+ (* requires { your code here } *)
+ ensures { !x = 10 }
+ =
+ while !x < 10 do (* variant { your code here } *)
+ (* invariant { your code here } *)
+ x := !x + 1
+ done;
+ x
+end
+
+module WeakenStrenghtenRef
+
+ use int.Int
+ use ref.Ref
+
+ let weaken_post (x: ref int) : ref int
+ requires { !x < 10 }
+ ensures { !result < 20 } (* too weak for !x < 10 *)
+ =
+ x
+
+ let strenghten_pre (x: ref int) : ref int
+ requires { !x < 0 } (* too strong for !x < 10 *)
+ ensures { !result < 20 }
+ =
+ x:= !(weaken_post x);
+ x
+end
+
+
+
+
+theory Imp
+
+ use state.State
+ use bool.Bool
+ use int.Int
+
+ type cond = state -> bool
+
+ (* ************************ SYNTAX ************************ *)
+ type aexpr =
+ | Anum int
+ | Avar id
+ | Aadd aexpr aexpr
+ | Asub aexpr aexpr
+
+ type bexpr =
+ | Btrue
+ | Bfalse
+ | Band bexpr bexpr
+ | Bnot bexpr
+ | Beq aexpr aexpr
+ | Ble aexpr aexpr
+
+ type com =
+ | Cskip
+ | Cassign id aexpr
+ | Cseq com com
+ | Cif bexpr com com
+ | Cwhile bexpr cond com (* <-- cond is the loop invaraint *)
+
+ (* ************************ SEMANTICS ************************ *)
+ function aeval (st : state) (e : aexpr) : int =
+ match e with
+ | Anum n -> n
+ | Avar x -> st[x]
+ | Aadd e1 e2 -> aeval st e1 + aeval st e2
+ | Asub e1 e2 -> aeval st e1 - aeval st e2
+ end
+ meta "rewrite_def" function aeval
+
+ function beval (st : state) (b : bexpr) : bool =
+ match b with
+ | Btrue -> true
+ | Bfalse -> false
+ | Bnot b -> notb (beval st b)
+ | Band b1 b2 -> andb (beval st b1) (beval st b2)
+ | Beq a1 a2 -> aeval st a1 = aeval st a2
+ | Ble a1 a2 -> aeval st a1 <= aeval st a2
+ end
+ meta "rewrite_def" function beval
+
+end
+
+module HoareRules
+
+ meta compute_max_steps 0x10000
+
+ use export Imp
+ use export state.State
+ use export bool.Bool
+ use export int.Int
+
+ constant triv_cond : cond = fun _ -> true
+
+ function wp (com : com) (q : cond) : cond =
+ match com with
+ | Cskip -> q
+ | Cassign id a -> fun s -> q s[id <- aeval s a]
+ | Cseq c1 c2 -> wp c1 (wp c2 q)
+ | Cif b ct cf -> fun s ->
+ (beval s b -> wp ct q s) /\
+ (not (beval s b) -> wp cf q s)
+ | Cwhile _ i _ -> i
+ end
+ meta "rewrite_def" function wp
+
+ function vc (com:com) (q : cond) : cond =
+ match com with
+ | Cskip -> triv_cond
+ | Cassign _ _ -> triv_cond
+ | Cseq c1 c2 -> fun s -> vc c1 (wp c2 q) s /\ vc c2 q s
+ | Cif _ ct cf -> fun s -> vc ct q s /\ vc cf q s
+ | Cwhile b i c -> fun s ->
+ ((i s /\ not (beval s b)) -> q s) /\ (* <-- postcond *)
+ ((i s /\ beval s b) -> wp c i s) /\ (* <-- invariant *)
+ vc c i s (* <-- body *)
+ end
+ meta "rewrite_def" function vc
+
+ function vcg (p : cond) (c : com) (q : cond) : cond =
+ fun s -> ((p s) -> ((wp c q) s)) /\ vc c q s
+ meta "rewrite_def" function vcg
+
+end
+
+module HoareTest
+
+ use HoareRules
+ use ref.Ref
+
+ constant a_id : id = Id 1
+ constant b_id : id = Id 2
+ constant c_id : id = Id 3
+
+
+ (* assignment command *)
+ let assignment (a : int)
+ requires { true }
+ ensures { !result = 2 }
+ =
+ let a = ref 0 in
+ a := 2;
+ a
+
+ (* derive weakest precondition *)
+ goal ass_wp : (* { true } a := 2 {a = 2} *)
+ let q = fun s -> s[a_id] = 2 in (* postcondition *)
+ let c = Cassign a_id (Anum 2) in (* assignment command *)
+ wp c q = triv_cond
+
+ (* forall s. p s -> p' s (* prove that p implies q *)
+ *)
+
+ (* derive and prove verification conditions *)
+ goal ass_vc : (* { true } a := 2 {a = 2} *)
+ let q = fun s -> s[a_id] = 2 in (* postcondition *)
+ let c = Cassign a_id (Anum 2) in (* assignment command *)
+ let vcs = vc c q in
+ forall s. vcs s (* prove vcs *)
+
+ (* both at the same time *)
+ goal ass : (* { true } a := 2 {a = 2} *)
+ let p = triv_cond in (* precondition *)
+ let q = fun s -> s[a_id] = 2 in (* postcondition *)
+ let c = Cassign a_id (Anum 2) in (* assignment command *)
+ forall s. (vcg p c q) s (* prove p -> q and vcs *)
+
+ (* sequence of assignment commands, with precondition *)
+ let seq_assignment (b : ref int)
+ requires { !b = 2 }
+ ensures { !result = 2 }
+ =
+ let a = ref 0 in
+ a := 4;
+ a := 2;
+ a
+
+ (* sequence of assignment commands, with precondition *)
+ goal seq_ass : (* b = 2 } a := 3; a := 2 {a = 2} *)
+ let p = fun s -> s[b_id] = 2 in (* precondition *)
+ let q = fun s -> s[a_id] = 2 in (* postcondition *)
+ (* sequence *)
+ let c = Cseq (Cassign a_id (Anum 3)) (Cassign a_id (Avar b_id)) in
+ forall s. (vcg p c q) s (* prove p -> q and vcs *)
+
+ let condition (b c : ref int)
+ requires { !c = 3 }
+ ensures { !result = 3 }
+ =
+ let a = ref 0 in
+ if !b = 0 then a := 3 else a := !c;
+ a
+
+ (* we cheat a bit, considering b = true and false separately *)
+ goal cond_true : (* { c = 3 } if true then a := 3 else a := {a = 3} *)
+ let p = fun s -> s[c_id] = 3 in (* precondition *)
+ let q = fun s -> s[a_id] = 3 in (* postcondition *)
+ let c = Cif Btrue (Cassign a_id (Anum 3)) (Cassign a_id (Avar c_id)) in
+ forall s. (vcg p c q) s (* prove p -> q and vcs *)
+
+ goal cond_false : (* { c = 3 } if false then a := 3 else a := b {a = 3} *)
+ let p = fun s -> s[c_id] = 3 in (* precondition *)
+ let q = fun s -> s[a_id] = 3 in (* postcondition *)
+ let c = Cif Bfalse (Cassign a_id (Anum 3)) (Cassign a_id (Avar c_id)) in
+ forall s. (vcg p c q) s (* prove p -> q and vcs *)
+
+(*
+ (* finish and prove the program below *)
+
+ goal cond : (* { c = 3 } if false then a := 3 else a := b {a = 3} *)
+ let p = fun s -> s[c_id] = 3 in (* precondition *)
+ let q = fun s -> s[a_id] = 3 in (* postcondition *)
+ let c = Cif (* your code here *)
+ (Cassign a_id (Anum 3)) (Cassign a_id (Avar c_id)) in
+ forall s. (vcg p c q) s (* prove p -> q and vcs *)
+*)
+
+ (* loop *)
+ let looping a b
+ requires { !a = 0 /\ !b = 2 }
+ ensures { !result = !b + 1 }
+ =
+ while !a <= !b do variant { !b - !a }
+ invariant { !a <= !b + 1 }
+ a := !a + 1;
+ done;
+ a
+
+ (*
+ split the verication conditions into sepratate subgoals
+ alt-ergo should discharge all 4
+
+ invalidate the precondition, !a = 7,
+ what conditions are now discharged and why
+
+ restore into orig state, and invalidate the loop invariant
+ !a <= b, what conditions are now discharged and why
+ !a <= b + 2, what conditions are now discharged and why
+
+ restore into orig stata, and invalitade the loop body
+ a := !a + 2, what condititons are now discharged and why
+ *)
+
+
+ (*
+ similarly we can encode the problem in "imp"
+ proof context (Task) can be understood as follows
+
+ -- transformations
+ compute_specified (computes the vcg and vc)
+ split_vc (splits and introduces premises)
+
+ see if you can relate the generated vcs to that of the "imp" program.
+
+ vc [0] invariant_init
+ axiom H1 : s[a_id] = 0
+ axiom H : s[b_id] = 2
+ ------------------------------- Goal --------------------------------
+ goal loo : s[a_id] <= (s[b_id] + 1)
+
+ vc [1] post_confition, given by the "while false" case
+ axiom H1 : s[a_id] <= (s[b_id] + 1)
+ axiom H : not s[a_id] <= s[b_id]
+
+ -- H not s[a_id] <= s[b_id] -> s[b_id] < s[a_id]
+ -- H1 states s[a_id] <= s[b_id] + 1, thus H,H1 -> s[a_id] = s[b_id] + 1
+ ------------------------------- Goal --------------------------------
+ goal loo : s[a_id] = (s[b_id] + 1)
+
+ vc [2] invariant preservation
+ axiom H1 : s[a_id] <= (s[b_id] + 1) (loop invariant)
+ axiom H : s[a_id] <= s[b_id] (loop condition)
+ -- informally the loop condition implies the invariant
+ ------------------------------- Goal --------------------------------
+ s[a_id <- (s[a_id] + 1)][a_id] <= (s[a_id <- (s[a_id] + 1)][b_id] + 1)
+
+ vc [3] vc for the loop body
+ -- trivial no vc generated for assignments in loop body
+ *)
+
+ goal loo:
+ (*
+ { a = 0 /\ b = 2 }
+ [ while a <= b {a <= b + 1} do a := a + 1; ]
+ { a = b + 1 }
+ *)
+ let p = fun s -> s[a_id] = 0 /\ s[b_id] = 2 in (* precondition *)
+ let q = fun s -> s[a_id] = s[b_id] + 1 in (* postcondition *)
+ let i = fun s -> s[a_id] <= s[b_id] + 1 in (* loop invariant *)
+ let c =
+ Cwhile (Ble (Avar a_id) (Avar b_id)) i (
+ Cassign a_id (Aadd (Avar a_id) (Anum 1))
+ ) in
+
+ forall s. (vcg p c q) s (* prove p -> q and vcs *)
+
+
+
+end
+
diff --git a/hoare/hoare_logic/why3session.xml b/hoare/hoare_logic/why3session.xml
new file mode 100644
index 0000000000000000000000000000000000000000..832cae013199931fc28ab87aa1c35f0c1d281b58
--- /dev/null
+++ b/hoare/hoare_logic/why3session.xml
@@ -0,0 +1,221 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<file name="../state.mlw" proved="true">
+<theory name="State" proved="true">
+ <goal name="VC get" expl="VC for get" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC set" expl="VC for set" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix []" expl="VC for mixfix []" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix [<-]" expl="VC for mixfix [<-]" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="Reg" proved="true">
+ <goal name="VC read" expl="VC for read" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC write" expl="VC for write" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../hoare_logic.mlw">
+<theory name="Sum" proved="true">
+ <goal name="s0" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+ <goal name="s1" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
+ </goal>
+ <goal name="s2" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
+ </goal>
+ <goal name="s3" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
+ </goal>
+ <goal name="sumf_lem" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="f0" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
+ </goal>
+ <goal name="f1" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
+ </goal>
+ <goal name="f2" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="f3" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="VC sum_whyML_rec" expl="VC for sum_whyML_rec" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="29"/></proof>
+ </goal>
+ <goal name="VC sum_whyML" expl="VC for sum_whyML" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="25"/></proof>
+ </goal>
+ <goal name="VC ml0" expl="VC for ml0" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="VC ml1" expl="VC for ml1" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="VC ml2" expl="VC for ml2" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+ <goal name="VC ml3" expl="VC for ml3" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+</theory>
+<theory name="Assignment">
+ <goal name="VC f" expl="VC for f" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC g" expl="VC for g">
+ </goal>
+</theory>
+<theory name="AssignmentRef">
+ <goal name="VC f" expl="VC for f" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC g" expl="VC for g">
+ </goal>
+</theory>
+<theory name="SequenceRef">
+ <goal name="VC seq" expl="VC for seq">
+ </goal>
+</theory>
+<theory name="WhileRef">
+ <goal name="VC loop" expl="VC for loop">
+ </goal>
+</theory>
+<theory name="WeakenStrenghtenRef" proved="true">
+ <goal name="VC weaken_post" expl="VC for weaken_post" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+ <goal name="VC strenghten_pre" expl="VC for strenghten_pre" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="HoareTest" proved="true">
+ <goal name="VC assignment" expl="VC for assignment" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="VC assignment.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ass_wp" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="ass_wp.0" proved="true">
+ <transf name="compute_specified" proved="true" >
+ <goal name="ass_wp.0.0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ass_vc" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="ass_vc.0" proved="true">
+ <transf name="introduce_premises" proved="true" >
+ <goal name="ass_vc.0.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ass" proved="true">
+ <transf name="compute_specified" proved="true" >
+ <goal name="ass.0" proved="true">
+ <transf name="split_goal_right" proved="true" >
+ <goal name="ass.0.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
+ </goal>
+ <goal name="ass.0.1" proved="true">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="VC seq_assignment" expl="VC for seq_assignment" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="VC seq_assignment.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="seq_ass" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="VC condition" expl="VC for condition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
+ </goal>
+ <goal name="cond_true" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="66"/></proof>
+ </goal>
+ <goal name="cond_false" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="66"/></proof>
+ </goal>
+ <goal name="VC looping" expl="VC for looping" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
+ </goal>
+ <goal name="loo" proved="true">
+ <transf name="compute_specified" proved="true" arg1="vcg">
+ <goal name="loo.0" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="loo.0.0" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.0.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="loo.0.1" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.1.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="loo.0.2" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.2.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="loo.0.3" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.3.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/hoare/hoare_logic/why3session.xml.bak b/hoare/hoare_logic/why3session.xml.bak
new file mode 100644
index 0000000000000000000000000000000000000000..0059549b03b86e1cafa73e293fd6b612363b4383
--- /dev/null
+++ b/hoare/hoare_logic/why3session.xml.bak
@@ -0,0 +1,221 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/>
+<file name="../state.mlw" proved="true">
+<theory name="State" proved="true">
+ <goal name="VC get" expl="VC for get" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC set" expl="VC for set" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix []" expl="VC for mixfix []" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix [<-]" expl="VC for mixfix [<-]" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="Reg" proved="true">
+ <goal name="VC read" expl="VC for read" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC write" expl="VC for write" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../hoare_logic.mlw">
+<theory name="Sum" proved="true">
+ <goal name="s0" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+ <goal name="s1" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
+ </goal>
+ <goal name="s2" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
+ </goal>
+ <goal name="s3" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
+ </goal>
+ <goal name="sumf_lem" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="f0" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
+ </goal>
+ <goal name="f1" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
+ </goal>
+ <goal name="f2" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="f3" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="VC sum_whyML_rec" expl="VC for sum_whyML_rec" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="29"/></proof>
+ </goal>
+ <goal name="VC sum_whyML" expl="VC for sum_whyML" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="25"/></proof>
+ </goal>
+ <goal name="VC ml0" expl="VC for ml0" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="VC ml1" expl="VC for ml1" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="VC ml2" expl="VC for ml2" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+ <goal name="VC ml3" expl="VC for ml3" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+</theory>
+<theory name="Assignment">
+ <goal name="VC f" expl="VC for f" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC g" expl="VC for g">
+ <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ <proof prover="2"><result status="unknown" time="0.00"/></proof>
+ </goal>
+</theory>
+<theory name="AssignmentRef">
+ <goal name="VC f" expl="VC for f" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC g" expl="VC for g">
+ <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ </goal>
+</theory>
+<theory name="SequenceRef">
+ <goal name="VC seq" expl="VC for seq">
+ <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ </goal>
+</theory>
+<theory name="WhileRef">
+ <goal name="VC loop" expl="VC for loop">
+ <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ </goal>
+</theory>
+<theory name="WeakenStrenghtenRef" proved="true">
+ <goal name="VC weaken_post" expl="VC for weaken_post" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+ <goal name="VC strenghten_pre" expl="VC for strenghten_pre" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="HoareTest">
+ <goal name="VC assignment" expl="VC for assignment">
+ <transf name="split_vc" >
+ <goal name="VC assignment.0" expl="postcondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ass_wp" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="ass_wp.0" proved="true">
+ <transf name="compute_specified" proved="true" >
+ <goal name="ass_wp.0.0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ass_vc">
+ <transf name="subst_all" >
+ <goal name="ass_vc.0">
+ <transf name="introduce_premises" >
+ <goal name="ass_vc.0.0">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ass">
+ <transf name="compute_specified" >
+ <goal name="ass.0">
+ <transf name="split_goal_right" >
+ <goal name="ass.0.0">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="10"/></proof>
+ </goal>
+ <goal name="ass.0.1">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="VC seq_assignment" expl="VC for seq_assignment">
+ <transf name="split_vc" >
+ <goal name="VC seq_assignment.0" expl="postcondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="7"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="seq_ass">
+ </goal>
+ <goal name="VC condition" expl="VC for condition">
+ </goal>
+ <goal name="cond_true">
+ </goal>
+ <goal name="cond_false">
+ </goal>
+ <goal name="VC looping" expl="VC for looping">
+ </goal>
+ <goal name="loo" proved="true">
+ <transf name="compute_specified" proved="true" arg1="vcg">
+ <goal name="loo.0" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="loo.0.0" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.0.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="loo.0.1" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.1.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="loo.0.2" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.2.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="loo.0.3" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="loo.0.3.0" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/hoare/hoare_logic/why3shapes.gz b/hoare/hoare_logic/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..7a441d14552aac7685206e58dee48816912aeeb7
Binary files /dev/null and b/hoare/hoare_logic/why3shapes.gz differ
diff --git a/hoare/hoare_logic/why3shapes.gz.bak b/hoare/hoare_logic/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..7a441d14552aac7685206e58dee48816912aeeb7
Binary files /dev/null and b/hoare/hoare_logic/why3shapes.gz.bak differ
diff --git a/hoare/state.mlw b/hoare/state.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..ae308026575769c2e25e6dca1cf279766b3ac288
--- /dev/null
+++ b/hoare/state.mlw
@@ -0,0 +1,45 @@
+
+module State
+
+ use int.Int
+
+ type id = Id int
+ type state = id -> int
+
+ let function get (f: state) (x: id) = f x
+
+ let function set (f: state) (x: id) (v: int) : state =
+ fun (y: id) ->
+ match (x, y) with
+ | (Id xv, Id yv) -> if xv = yv then v else (f y)
+ end
+ (* meta rewrite_def function set *)
+
+ let function ([]) f x = f x
+ let function ([<-]) f x v = set f x v
+
+ let function const (v: int) : state
+ ensures { forall x. result[x] = v }
+ = fun _ -> v
+
+end
+
+module Reg
+
+ use int.Int
+
+ type idr = int
+ type regs = idr -> int
+
+ let function read (f: regs) (x: idr) = f x
+
+ let function write (f: regs) (x: idr) (v: int) : regs =
+ fun (y: idr) -> if x = y then v else (f y)
+
+ meta rewrite_def function write
+
+ let function const (v: int) : regs
+ ensures { forall x. read result x = v }
+ = fun _ -> v
+
+end
\ No newline at end of file