Skip to content
Snippets Groups Projects
Commit e6809fcc authored by Per Lindgren's avatar Per Lindgren
Browse files

examples for lecture 9, hoare_logic

parent 103edf0c
No related branches found
No related tags found
No related merge requests found
.DS_Store 0 → 100644
File added
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
<?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 [&lt;-]" 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>
<?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 [&lt;-]" 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>
File added
File added
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment