subsubsection"VCG for Total Correctness With Logical Variables"
theory VCG_Total_EX2 imports Hoare_Total_EX2 begin
text‹ ‹ a VCG built on top of a Hoare logic without logical variables.
a result the completeness proof runs into a problem. This theory uses a Hoare logic
logical variables and proves soundness and completeness. ›
‹Annotated commands: commands where loops are annotated with
.›
strip :: "acom → com" where
strip SKIP = SKIP" |
strip (x ::= a) = (x ::= a)" |
strip (C1;; C2) = (strip C1;; strip C2)" |
strip (IF b THEN C1 ELSE C2) = (IF b THEN strip C1 ELSE strip C2)" |
strip ({_/_} WHILE b DO C) = (WHILE b DO strip C)"
‹Weakest precondition from annotated commands:›
pre :: "acom → assn2 → assn2" where
pre SKIP Q = Q" |
pre (x ::= a) Q = (λl s. Q l (s(x := aval a s)))" |
pre (C1;; C2) Q = pre C1 (pre C2 Q)" |
pre (IF b THEN C1 ELSE C2) Q =
(λl s. if bval b s then pre C1 Q l s else pre C2 Q l s)" |
pre ({I/x} WHILE b DO C) Q = (λl s. ∃n. I (l(x:=n)) s)"
‹Verification condition:›
vc :: "acom → assn2 → bool" where
vc SKIP Q = True" |
vc (x ::= a) Q = True" |
vc (C1;; C2) Q = (vc C1 (pre C2 Q) ∧ vc C2 Q)" |
vc (IF b THEN C1 ELSE C2) Q = (vc C1 Q ∧ vc C2 Q)" |
vc ({I/x} WHILE b DO C) Q =
(∀l s. (I (l(x:=Suc(l x))) s ⟶ pre C I l s) ∧
(l x > 0 ∧ I l s ⟶ bval b s) ∧
(I (l(x := 0)) s ⟶¬ bval b s ∧ Q l s) ∧
vc C I)"
vc_sound: "vc C Q ==>⊨t {pre C Q} strip C {Q}"
(induction C arbitrary: Q)
case (Awhile I x b C)
show ?case
proof(simp, rule weaken_post[OF While[of I x]], goal_cases)
case 1 show ?case
using Awhile.IH[of "I"] Awhile.prems by (auto intro: strengthen_pre)
next
case 3 show ?case
using Awhile.prems by (simp) (metis fun_upd_triv)
qed (insert Awhile.prems, auto)
(auto intro: conseq Seq If simp: Skip Assign)
‹Completeness:›
pre_mono:
"∀l s. P l s ⟶ P' l s ==> pre C P l s ==> pre C P' l s"
(induction C arbitrary: P P' l s)
case Aseq thus ?case by simp metis
simp_all
vc_mono:
"∀l s. P l s ⟶ P' l s ==> vc C P ==> vc C P'"
(induction C arbitrary: P P')
case Aseq thus ?case by simp (metis pre_mono)
simp_all
vc_complete:
"⊨t {P}c{Q} ==>∃C. strip C = c ∧ vc C Q ∧ (∀l s. P l s ⟶ pre C Q l s)"
(is "_ ==>∃C. ?G P c Q C")
(induction rule: hoaret.induct)
case Skip
show ?case (is "∃C. ?C C")
proof show "?C Askip" by simp qed
case (Assign P a x)
show ?case (is "∃C. ?C C")
proof show "?C(Aassign x a)" by simp qed
case (Seq P c1 Q c2 R)
from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast
from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast
show ?case (is "∃C. ?C C")
proof
show "?C(Aseq C1 C2)"
using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
qed
case (If P b c1 Q c2)
from If.IH obtain C1 where ih1: "?G (λl s. P l s ∧ bval b s) c1 Q C1"
by blast
from If.IH obtain C2 where ih2: "?G (λl s. P l s ∧¬bval b s) c2 Q C2"
by blast
show ?case (is "∃C. ?C C")
proof
show "?C(Aif b C1 C2)" using ih1 ih2 by simp
qed
case (While P x c b)
from While.IH obtain C where
ih: "?G (λl s. P (l(x:=Suc(l x))) s ∧ bval b s) c P C"
by blast
show ?case (is "∃C. ?C C")
proof
have "vc ({P/x} WHILE b DO C) (λl. P (l(x := 0)))"
using ih While.hyps(2,3)
by simp (metis fun_upd_same zero_less_Suc)
thus "?C(Awhile P x b C)" using ih by simp
qed
case conseq thus ?case by(fast elim!: pre_mono vc_mono)
‹Two examples:›
vc1: "vc
({λl s. l ''x'' = nat(s ''x'') / ''x''} WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1)))
(λl s. s ''x'' ≤ 0)"
auto
vc_sound[OF vc1, simplified]
vc2: "vc
({λl s. l ''x'' = nat(s ''x'') / ''x''} WHILE Less (N 0) (V ''x'')
DO (''x'' ::= Plus (V ''x'') (N (-1));;
(''y'' ::= V ''x'';;
{λl s. l ''x'' = nat(s ''x'') ∧ l ''y'' = nat(s ''y'') / ''y''}
WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1)))))
λl s. s ''x'' ≤ 0)"
auto
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
