# Theory VCG

theory VCG
imports Hoare
```(* Author: Tobias Nipkow *)

theory VCG imports Hoare begin

subsection "Verification Conditions"

text{* Annotated commands: commands where loops are annotated with
invariants. *}

datatype acom =
Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)

notation com.SKIP ("SKIP")

text{* Strip annotations: *}

fun strip :: "acom ⇒ com" where
"strip SKIP = SKIP" |
"strip (x ::= a) = (x ::= a)" |
"strip (C⇩1;; C⇩2) = (strip C⇩1;; strip C⇩2)" |
"strip (IF b THEN C⇩1 ELSE C⇩2) = (IF b THEN strip C⇩1 ELSE strip C⇩2)" |
"strip ({_} WHILE b DO C) = (WHILE b DO strip C)"

text{* Weakest precondition from annotated commands: *}

fun pre :: "acom ⇒ assn ⇒ assn" where
"pre SKIP Q = Q" |
"pre (x ::= a) Q = (λs. Q(s(x := aval a s)))" |
"pre (C⇩1;; C⇩2) Q = pre C⇩1 (pre C⇩2 Q)" |
"pre (IF b THEN C⇩1 ELSE C⇩2) Q =
(λs. if bval b s then pre C⇩1 Q s else pre C⇩2 Q s)" |
"pre ({I} WHILE b DO C) Q = I"

text{* Verification condition: *}

fun vc :: "acom ⇒ assn ⇒ bool" where
"vc SKIP Q = True" |
"vc (x ::= a) Q = True" |
"vc (C⇩1;; C⇩2) Q = (vc C⇩1 (pre C⇩2 Q) ∧ vc C⇩2 Q)" |
"vc (IF b THEN C⇩1 ELSE C⇩2) Q = (vc C⇩1 Q ∧ vc C⇩2 Q)" |
"vc ({I} WHILE b DO C) Q =
((∀s. (I s ∧ bval b s ⟶ pre C I s) ∧
(I s ∧ ¬ bval b s ⟶ Q s)) ∧
vc C I)"

text {* Soundness: *}

lemma vc_sound: "vc C Q ⟹ ⊢ {pre C Q} strip C {Q}"
proof(induction C arbitrary: Q)
case (Awhile I b C)
show ?case
proof(simp, rule While')
from `vc (Awhile I b C) Q`
have vc: "vc C I" and IQ: "∀s. I s ∧ ¬ bval b s ⟶ Q s" and
pre: "∀s. I s ∧ bval b s ⟶ pre C I s" by simp_all
have "⊢ {pre C I} strip C {I}" by(rule Awhile.IH[OF vc])
with pre show "⊢ {λs. I s ∧ bval b s} strip C {I}"
by(rule strengthen_pre)
show "∀s. I s ∧ ¬bval b s ⟶ Q s" by(rule IQ)
qed
qed (auto intro: hoare.conseq)

corollary vc_sound':
"⟦ vc C Q; ∀s. P s ⟶ pre C Q s ⟧ ⟹ ⊢ {P} strip C {Q}"
by (metis strengthen_pre vc_sound)

text{* Completeness: *}

lemma pre_mono:
"∀s. P s ⟶ P' s ⟹ pre C P s ⟹ pre C P' s"
proof (induction C arbitrary: P P' s)
case Aseq thus ?case by simp metis
qed simp_all

lemma vc_mono:
"∀s. P s ⟶ P' s ⟹ vc C P ⟹ vc C P'"
proof(induction C arbitrary: P P')
case Aseq thus ?case by simp (metis pre_mono)
qed simp_all

lemma vc_complete:
"⊢ {P}c{Q} ⟹ ∃C. strip C = c ∧ vc C Q ∧ (∀s. P s ⟶ pre C Q s)"
(is "_ ⟹ ∃C. ?G P c Q C")
proof (induction rule: hoare.induct)
case Skip
show ?case (is "∃C. ?C C")
proof show "?C Askip" by simp qed
next
case (Assign P a x)
show ?case (is "∃C. ?C C")
proof show "?C(Aassign x a)" by simp qed
next
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
next
case (If P b c1 Q c2)
from If.IH obtain C1 where ih1: "?G (λs. P s ∧ bval b s) c1 Q C1"
by blast
from If.IH obtain C2 where ih2: "?G (λs. P 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
next
case (While P b c)
from While.IH obtain C where ih: "?G (λs. P s ∧ bval b s) c P C" by blast
show ?case (is "∃C. ?C C")
proof show "?C(Awhile P b C)" using ih by simp qed
next
case conseq thus ?case by(fast elim!: pre_mono vc_mono)
qed

end
```