From e6809fcc81da8feb7cfdf5d9271e691aff92e1fe Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 2 Oct 2018 08:54:57 +0200
Subject: [PATCH] examples for lecture 9, hoare_logic
---
.DS_Store | Bin 0 -> 6148 bytes
hoare/hoare_logic.mlw | 410 ++++++++++++++++++++++++++
hoare/hoare_logic/why3session.xml | 221 ++++++++++++++
hoare/hoare_logic/why3session.xml.bak | 221 ++++++++++++++
hoare/hoare_logic/why3shapes.gz | Bin 0 -> 2392 bytes
hoare/hoare_logic/why3shapes.gz.bak | Bin 0 -> 2392 bytes
hoare/state.mlw | 45 +++
7 files changed, 897 insertions(+)
create mode 100644 .DS_Store
create mode 100644 hoare/hoare_logic.mlw
create mode 100644 hoare/hoare_logic/why3session.xml
create mode 100644 hoare/hoare_logic/why3session.xml.bak
create mode 100644 hoare/hoare_logic/why3shapes.gz
create mode 100644 hoare/hoare_logic/why3shapes.gz.bak
create mode 100644 hoare/state.mlw
diff --git a/.DS_Store b/.DS_Store
new file mode 100644
index 0000000000000000000000000000000000000000..90bd44924b79ec5d54f3687165c3746c4a239273
GIT binary patch
literal 6148
zcmZQzU|@7AO)+F(5MW?n;9!8zEL;p&0Z1N%F(jFwA|RR(Y(@b?4nrzKaZ-740aR|3
z8V!Nb5E#560Lr@@45<ti42cZ63`qGmDJMUPfq~&?QbA5;afyM!O-3eW7FITP4o)sG
z5D*lK4bI3f4=zb8DJ^zNEQ$v6GE-8MpzMIek_;F-BtJg~&Q44U%S<hg7Z7pI&nrpH
z%u6jo(i#(<nU|7Z?v!7emr@)P3^6Y}Go>UWUO+UUD77pzwLBm(FEuQ)I5R0TC$prI
z6Aa=7B&w@TjZAeEjExLxbrh=2%?)%EOpMKIYXuH)a7b&KI{HQy)OIaeykzOJ<tq*!
zg~SOXBZOuUhSD(V7y|<XD?<iDK0_iy5ko4dNE?ztVr*=rqhM}mL8Typ1<xow^g{re
z^f|bPzE?(lFd71*AwcC20F@64puPeF1A_yUZh+7rDF#Lc22k?>M6<xGhV%m%Kw==R
zAR43<M1!<4FoIZMGr(FI7#Sd18NuBUkUmhC1Vn?iGcbZ}2Jyk#8DRA_BSbp`BSbp`
zBeaLY2+_{K2+_{K2(}&Ox>0&G1V%#u76Qx=h5)GkcV%F})&Ga68YM?VU^E1VWe6~`
zxCFa6fh%R~{sYyup!zfcDh;arLDexMs9uKX11SN^GC>9uCBPhr97rpu+6Py~j0_AQ
St)mSASOAUEqaiQ=ApiibU$DUd
literal 0
HcmV?d00001
diff --git a/hoare/hoare_logic.mlw b/hoare/hoare_logic.mlw
new file mode 100644
index 0000000..fc3f515
--- /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 0000000..832cae0
--- /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 0000000..0059549
--- /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
GIT binary patch
literal 2392
zcmb2|=3oGW|7Rnkv!y-7>aMT<@Y|rk?=H8^hIxrBZ13%Kt0KjUUrp=qe6wb)%I5!d
z`@_7~PP(#b?u15Pk1MgE&x4--l0E5iyXeD{J?5v<PAj^|CUGWB7QVkOY=7+5<I7i<
zmu`-9SuEq-eZ^_3+wNttfePj8Oti1P;kV~+-?~vGcfqq{q4`cLk4;^(ckR-ZQ<fi=
zzh1xX>-_Nlzsx<>tkp3L>k4!Y4mpr~;?9lsWl@%@JO4?#EESbK(fXpKSgZBTl3hVr
z-A>oqcd4K1=RYqUY0ood{|S|?e%_Ct-w(@L8onjQ@L#l^&x)Yg=YrOJJ1Z`o8?>Wp
zqu#VLiRb^W^t!3jGbP9+JnQE63BCqXW}jV_p{y|f-Jh?SdsohO?TE?kUHC*GNN{TK
zDyypW5|P!jXNA`aeC@h6D@o7wr9$A-1*<>Je6aYAM%ATNF(*Gi@1JR;yQSU5%*|MM
z_64t^P??nyYt23HR7@&Qs$=5SkC?dCP<v|0>0?V4<*w<>>f5LK{Hn*|Zzi_6VchXv
zPA(yyH>Kjer_AC$n6+%%oNSquUp2oPPG2K_$!X#-j<r&gKH61oJ0!!=)iC+yr^t(4
z`QNuiecW&*Y)kykf2zW7wsM?3cA-Pi*>vVI?yG8(oP;t@@rd7wu3m8emTzG5)DOo6
z_Z+p8diWsutLcwfi|iCF%@Wpmvd-37_c|!#+(du2^gX>^+h_T8=tm0W>~YgL61LUk
zhO+ykn6;lgQj+WvKkxGNJ{7g{)u!uLT|=ETBY8HjEtnW?^7Q-j{_pYk|9^j9{@ven
ze&qKwqd&WD-##g|=u2AEHRVnzPk}@G@4x+47k4qmWJ3C^d5M3Y`o4EC-n;fp<Ifkj
zmCLsOe=&0o8{?*1%1hUtTQY~2Q8G|w(zU|AQ!^^cetvyA+uu6v&PDdMRm?fAuP1ty
zf1hEyrP?|sW9jbntMc!!=Uc~qvwJW#?p~SSjrFU~oNnfOb)szf^tUXB3Xk9N`}brz
zpKqLuiJb838<l^f<$A5{V(dy@T~QL0>lG^PN%2~i5^%jFBuGYj)~(ye`Ax*7D`uM9
z_KKH1F306K`I3(`*CM5KT}#Kr62YSeOYfXnm|pw9k7>T=gFvSFUJqO!y$JSZI?I`P
z?rf!r$`{diAIF219szS%YSj|Ic!ez&x^ie+h_q#&;8c;TErBeXlII6ZRoY!MVSzR0
zJD)=mry}QjUFhyAYg@N8@I_W}+vNqdJO@`jVzo`yU${_HEPJic0l^sS4B4&A+w5jt
zFumY@xy57In&&xuKPO85EH`g8;pzDGj@wITfs1#mY5MH0%|{oNF+K@6IrqznJ53k6
z0-Z~FB#)gx<GDj)d6QoL#Cy-Z)*mlw{Pu2+MS9G%hI^siUqxdNyb3uvi_hV2`lE#h
z{vQyu+`8vX{9@MZ7=87mx1}-@#27-dbr~yuzFZ_PCvX4tqDOG%o_qW5nY_p<k(=P5
z<7u)XG-#_@pcYH>go3<7Mxp;!@PD5#r`}=oA)r0vPEm|rO2+k!e;&4H8A9|tCbC#W
z<a$~8COohF93p>j?|mMd`LB++l<M@KHQ3=$Drg?JqPn?YvB33%Y>Dmf;w(0AdhuCr
zby8GlaKOpWpMTvweEipjmuD_t4cMb2E~sH_;g+J|SX^*6{dE-AnziMIpROiwCv4kv
zZ;ibCGBurG<@<K}JPuioHP<gNT=e2H)%Y^6XIuBzYmOc3=d;DA&tCp@`tQc~bN`rW
zX%+3)EBb7(<m+8VVZR4rTWc*QUKR1Pjhj+$SG(@CtJ|&HVLA`$!{itaFj!XWg&BxV
z;9XvICh7dd>y8_v8y-&=*?e2LxJ&X)Z`V$N6D;i9*ELpDv&~@3%xG;=%F7LU6Qi8+
zFlySThdc8s=V~k5<!LmLntHQVCw|AnMVi@MS%$m`{WlcX%`thN^;Pcak@&qSbM-3?
z9^Ag0uD|Pj!cwN3`3=>kj(gZxuHEwfB6Otq=!cKKTz@&XOL|?~a%if+@pD0wJ?4po
zE@?XyP`FHBOU1P3x?dNy+*<Wx!J?$YirURQ!rh4nkEiWCE4W{};2cAiU-Jj{8Q<Sc
zDCK_8Ay&Ywdan3$TW>DgOrF(?jW<|d&t2sDjqgof9H+}I%`Lxo)J|30WS;Rv^F!rP
zm!lqhZoNS-<|^_C>W16LEs=V5GQo>m(WU?A4ad$SD{31wLqESRW9V0S5!hLB&_dSp
zc-#JjWZx3AY5Rolofk>HDxSLMi>=}8r=ADPmd%==yZnlQl$uj*^CcI@30tC;Zx?;@
z?xxRq&Q=-I+iqVxvSrRRYF=T8N%CxMY23ZXFs*%Fz1)spDQ~-NJP%ziKmJ)}?)^=3
z78l=;mVNe6;*{V5jtwU#R><#lK6*J!vo~|)?{!Hgk9U1O&)HzvBlnjtZra@YE6P{8
zE$BXZSlnwJQ_^*bDGL<0$aF2d@!-Vv$jZA<uAjXicrWeMpRSc(x6ihUU+~)Jtqr4C
zrAk51v1M(q;@TSbbn@PuzWx4|T<Zt_KZf=OvkDk9vHWaldo^pbou{Fpb<5OOjIVz^
zj1><S{`B-^b<^v*X;05QH#ROeHjbY$bLae-`sa?ZPpPk6<YWG8&5HXk9!JXVW4`(5
zve&AkPFK5@E-ab-s&R*{m&(S2H%d-Em3lSn<kR^3>+M5+ivHgwXS+_~!lxTAgS_hV
zI=JV_RNk$=)azbWZh7m57@uAF#-sP1Uf`H6(bmml`%TX{<<`^<Gx@A@@|0(s+j%Up
z`1(YFRel`FjsllF+Y^_#uN7u2P!zv^@9z5ecUz6G-_txH{%!xnlNpC@Tl&B2_}%*O
z%baKWoKmW1ZvF~gba=_n>94=$hHT%weWy(5?*&eutYo(a2(7Q}T@km+t8d!szL{S0
z3LXZ=*u;PO`q^*3<ehD|gEmJmHsj_uiRcL3#PTBd#;Z9|!E$G<!(G0zrsnYr)mz;S
z5T9~0@2vLbxk7BIF^Y@cuuquIo1GL=_2Ai@q!pHD8!w0R8jCwrueyBse(KLwqbEWE
z^Mp-Q({F!Z4tdP*!(-pBC(o|d9c>Z6axZA^ynlM~x=G#=ccaTfmp0tsmbn=3%5ZCk
z%eKwy-g}+)o>p00Tg5zi@sEG6_joV}Yzw&D!sfM7DEmP1(QO5vei=yaP3W7hWA~ts
z`}h4bF0n?(`Fr{V7&LE8z0-4gV(r(%`O&Hej1KeL=zrb*x8PlaQ}3}KSJoKrsxmn)
g6FTjb8Y|y(<_~Ygjg$A^{rpG%n8?CSjdBbO0Ed~WPXGV_
literal 0
HcmV?d00001
diff --git a/hoare/hoare_logic/why3shapes.gz.bak b/hoare/hoare_logic/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..7a441d14552aac7685206e58dee48816912aeeb7
GIT binary patch
literal 2392
zcmb2|=3oGW|7Rnkv!y-7>aMT<@Y|rk?=H8^hIxrBZ13%Kt0KjUUrp=qe6wb)%I5!d
z`@_7~PP(#b?u15Pk1MgE&x4--l0E5iyXeD{J?5v<PAj^|CUGWB7QVkOY=7+5<I7i<
zmu`-9SuEq-eZ^_3+wNttfePj8Oti1P;kV~+-?~vGcfqq{q4`cLk4;^(ckR-ZQ<fi=
zzh1xX>-_Nlzsx<>tkp3L>k4!Y4mpr~;?9lsWl@%@JO4?#EESbK(fXpKSgZBTl3hVr
z-A>oqcd4K1=RYqUY0ood{|S|?e%_Ct-w(@L8onjQ@L#l^&x)Yg=YrOJJ1Z`o8?>Wp
zqu#VLiRb^W^t!3jGbP9+JnQE63BCqXW}jV_p{y|f-Jh?SdsohO?TE?kUHC*GNN{TK
zDyypW5|P!jXNA`aeC@h6D@o7wr9$A-1*<>Je6aYAM%ATNF(*Gi@1JR;yQSU5%*|MM
z_64t^P??nyYt23HR7@&Qs$=5SkC?dCP<v|0>0?V4<*w<>>f5LK{Hn*|Zzi_6VchXv
zPA(yyH>Kjer_AC$n6+%%oNSquUp2oPPG2K_$!X#-j<r&gKH61oJ0!!=)iC+yr^t(4
z`QNuiecW&*Y)kykf2zW7wsM?3cA-Pi*>vVI?yG8(oP;t@@rd7wu3m8emTzG5)DOo6
z_Z+p8diWsutLcwfi|iCF%@Wpmvd-37_c|!#+(du2^gX>^+h_T8=tm0W>~YgL61LUk
zhO+ykn6;lgQj+WvKkxGNJ{7g{)u!uLT|=ETBY8HjEtnW?^7Q-j{_pYk|9^j9{@ven
ze&qKwqd&WD-##g|=u2AEHRVnzPk}@G@4x+47k4qmWJ3C^d5M3Y`o4EC-n;fp<Ifkj
zmCLsOe=&0o8{?*1%1hUtTQY~2Q8G|w(zU|AQ!^^cetvyA+uu6v&PDdMRm?fAuP1ty
zf1hEyrP?|sW9jbntMc!!=Uc~qvwJW#?p~SSjrFU~oNnfOb)szf^tUXB3Xk9N`}brz
zpKqLuiJb838<l^f<$A5{V(dy@T~QL0>lG^PN%2~i5^%jFBuGYj)~(ye`Ax*7D`uM9
z_KKH1F306K`I3(`*CM5KT}#Kr62YSeOYfXnm|pw9k7>T=gFvSFUJqO!y$JSZI?I`P
z?rf!r$`{diAIF219szS%YSj|Ic!ez&x^ie+h_q#&;8c;TErBeXlII6ZRoY!MVSzR0
zJD)=mry}QjUFhyAYg@N8@I_W}+vNqdJO@`jVzo`yU${_HEPJic0l^sS4B4&A+w5jt
zFumY@xy57In&&xuKPO85EH`g8;pzDGj@wITfs1#mY5MH0%|{oNF+K@6IrqznJ53k6
z0-Z~FB#)gx<GDj)d6QoL#Cy-Z)*mlw{Pu2+MS9G%hI^siUqxdNyb3uvi_hV2`lE#h
z{vQyu+`8vX{9@MZ7=87mx1}-@#27-dbr~yuzFZ_PCvX4tqDOG%o_qW5nY_p<k(=P5
z<7u)XG-#_@pcYH>go3<7Mxp;!@PD5#r`}=oA)r0vPEm|rO2+k!e;&4H8A9|tCbC#W
z<a$~8COohF93p>j?|mMd`LB++l<M@KHQ3=$Drg?JqPn?YvB33%Y>Dmf;w(0AdhuCr
zby8GlaKOpWpMTvweEipjmuD_t4cMb2E~sH_;g+J|SX^*6{dE-AnziMIpROiwCv4kv
zZ;ibCGBurG<@<K}JPuioHP<gNT=e2H)%Y^6XIuBzYmOc3=d;DA&tCp@`tQc~bN`rW
zX%+3)EBb7(<m+8VVZR4rTWc*QUKR1Pjhj+$SG(@CtJ|&HVLA`$!{itaFj!XWg&BxV
z;9XvICh7dd>y8_v8y-&=*?e2LxJ&X)Z`V$N6D;i9*ELpDv&~@3%xG;=%F7LU6Qi8+
zFlySThdc8s=V~k5<!LmLntHQVCw|AnMVi@MS%$m`{WlcX%`thN^;Pcak@&qSbM-3?
z9^Ag0uD|Pj!cwN3`3=>kj(gZxuHEwfB6Otq=!cKKTz@&XOL|?~a%if+@pD0wJ?4po
zE@?XyP`FHBOU1P3x?dNy+*<Wx!J?$YirURQ!rh4nkEiWCE4W{};2cAiU-Jj{8Q<Sc
zDCK_8Ay&Ywdan3$TW>DgOrF(?jW<|d&t2sDjqgof9H+}I%`Lxo)J|30WS;Rv^F!rP
zm!lqhZoNS-<|^_C>W16LEs=V5GQo>m(WU?A4ad$SD{31wLqESRW9V0S5!hLB&_dSp
zc-#JjWZx3AY5Rolofk>HDxSLMi>=}8r=ADPmd%==yZnlQl$uj*^CcI@30tC;Zx?;@
z?xxRq&Q=-I+iqVxvSrRRYF=T8N%CxMY23ZXFs*%Fz1)spDQ~-NJP%ziKmJ)}?)^=3
z78l=;mVNe6;*{V5jtwU#R><#lK6*J!vo~|)?{!Hgk9U1O&)HzvBlnjtZra@YE6P{8
zE$BXZSlnwJQ_^*bDGL<0$aF2d@!-Vv$jZA<uAjXicrWeMpRSc(x6ihUU+~)Jtqr4C
zrAk51v1M(q;@TSbbn@PuzWx4|T<Zt_KZf=OvkDk9vHWaldo^pbou{Fpb<5OOjIVz^
zj1><S{`B-^b<^v*X;05QH#ROeHjbY$bLae-`sa?ZPpPk6<YWG8&5HXk9!JXVW4`(5
zve&AkPFK5@E-ab-s&R*{m&(S2H%d-Em3lSn<kR^3>+M5+ivHgwXS+_~!lxTAgS_hV
zI=JV_RNk$=)azbWZh7m57@uAF#-sP1Uf`H6(bmml`%TX{<<`^<Gx@A@@|0(s+j%Up
z`1(YFRel`FjsllF+Y^_#uN7u2P!zv^@9z5ecUz6G-_txH{%!xnlNpC@Tl&B2_}%*O
z%baKWoKmW1ZvF~gba=_n>94=$hHT%weWy(5?*&eutYo(a2(7Q}T@km+t8d!szL{S0
z3LXZ=*u;PO`q^*3<ehD|gEmJmHsj_uiRcL3#PTBd#;Z9|!E$G<!(G0zrsnYr)mz;S
z5T9~0@2vLbxk7BIF^Y@cuuquIo1GL=_2Ai@q!pHD8!w0R8jCwrueyBse(KLwqbEWE
z^Mp-Q({F!Z4tdP*!(-pBC(o|d9c>Z6axZA^ynlM~x=G#=ccaTfmp0tsmbn=3%5ZCk
z%eKwy-g}+)o>p00Tg5zi@sEG6_joV}Yzw&D!sfM7DEmP1(QO5vei=yaP3W7hWA~ts
z`}h4bF0n?(`Fr{V7&LE8z0-4gV(r(%`O&Hej1KeL=zrb*x8PlaQ}3}KSJoKrsxmn)
g6FTjb8Y|y(<_~Ygjg$A^{rpG%n8?CSjdBbO0Ed~WPXGV_
literal 0
HcmV?d00001
diff --git a/hoare/state.mlw b/hoare/state.mlw
new file mode 100644
index 0000000..ae30802
--- /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
--
GitLab