# Theory VC

Up to index of Isabelle/HOL/HOL-IMP

theory VC
imports Hoare
`(* Author: Tobias Nipkow *)theory VC imports Hoare beginsubsection "Verification Conditions"text{* Annotated commands: commands where loops are annotated withinvariants. *}datatype acom =  ASKIP |  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)text{* Weakest precondition from annotated commands: *}fun pre :: "acom => assn => assn" where"pre ASKIP Q = Q" |"pre (Aassign x a) Q = (λs. Q(s(x := aval a s)))" |"pre (Aseq c⇣1 c⇣2) Q = pre c⇣1 (pre c⇣2 Q)" |"pre (Aif b c⇣1 c⇣2) Q =  (λs. (bval b s --> pre c⇣1 Q s) ∧       (¬ bval b s --> pre c⇣2 Q s))" |"pre (Awhile I b c) Q = I"text{* Verification condition: *}fun vc :: "acom => assn => assn" where"vc ASKIP Q = (λs. True)" |"vc (Aassign x a) Q = (λs. True)" |"vc (Aseq c⇣1 c⇣2) Q = (λs. vc c⇣1 (pre c⇣2 Q) s ∧ vc c⇣2 Q s)" |"vc (Aif b c⇣1 c⇣2) Q = (λs. vc c⇣1 Q s ∧ vc c⇣2 Q s)" |"vc (Awhile I b c) Q =  (λs. (I s ∧ ¬ bval b s --> Q s) ∧       (I s ∧ bval b s --> pre c I s) ∧       vc c I s)"text{* Strip annotations: *}fun strip :: "acom => com" where"strip ASKIP = SKIP" |"strip (Aassign x a) = (x::=a)" |"strip (Aseq c⇣1 c⇣2) = (strip c⇣1; strip c⇣2)" |"strip (Aif b c⇣1 c⇣2) = (IF b THEN strip c⇣1 ELSE strip c⇣2)" |"strip (Awhile I b c) = (WHILE b DO strip c)"text {* Soundness: *}lemma vc_sound: "∀s. vc c Q s ==> \<turnstile> {pre c Q} strip c {Q}"proof(induction c arbitrary: Q)  case (Awhile I b c)  show ?case  proof(simp, rule While')    from `∀s. vc (Awhile I b c) Q s`    have vc: "∀s. vc c I s" 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 "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc])    with pre show "\<turnstile> {λ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)  qedqed (auto intro: hoare.conseq)corollary vc_sound':  "(∀s. vc c Q s) ∧ (∀s. P s --> pre c Q s) ==> \<turnstile> {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 metisqed simp_alllemma vc_mono:  "∀s. P s --> P' s ==> vc c P s ==> vc c P' s"proof(induction c arbitrary: P P')  case Aseq thus ?case by simp (metis pre_mono)qed simp_alllemma vc_complete: "\<turnstile> {P}c{Q} ==> ∃c'. strip c' = c ∧ (∀s. vc c' Q s) ∧ (∀s. P s --> pre c' Q s)"  (is "_ ==> ∃c'. ?G P c Q c'")proof (induction rule: hoare.induct)  case Skip  show ?case (is "∃ac. ?C ac")  proof show "?C ASKIP" by simp qednext  case (Assign P a x)  show ?case (is "∃ac. ?C ac")  proof show "?C(Aassign x a)" by simp qednext  case (Seq P c1 Q c2 R)  from Seq.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast  from Seq.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast  show ?case (is "∃ac. ?C ac")  proof    show "?C(Aseq ac1 ac2)"      using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)  qednext  case (If P b c1 Q c2)  from If.IH obtain ac1 where ih1: "?G (λs. P s ∧ bval b s) c1 Q ac1"    by blast  from If.IH obtain ac2 where ih2: "?G (λs. P s ∧ ¬bval b s) c2 Q ac2"    by blast  show ?case (is "∃ac. ?C ac")  proof    show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp  qednext  case (While P b c)  from While.IH obtain ac where ih: "?G (λs. P s ∧ bval b s) c P ac" by blast  show ?case (is "∃ac. ?C ac")  proof show "?C(Awhile P b ac)" using ih by simp qednext  case conseq thus ?case by(fast elim!: pre_mono vc_mono)qedtext{* An Optimization: *}fun vcpre :: "acom => assn => assn × assn" where"vcpre ASKIP Q = (λs. True, Q)" |"vcpre (Aassign x a) Q = (λs. True, λs. Q(s[a/x]))" |"vcpre (Aseq c⇣1 c⇣2) Q =  (let (vc⇣2,wp⇣2) = vcpre c⇣2 Q;       (vc⇣1,wp⇣1) = vcpre c⇣1 wp⇣2   in (λs. vc⇣1 s ∧ vc⇣2 s, wp⇣1))" |"vcpre (Aif b c⇣1 c⇣2) Q =  (let (vc⇣2,wp⇣2) = vcpre c⇣2 Q;       (vc⇣1,wp⇣1) = vcpre c⇣1 Q   in (λs. vc⇣1 s ∧ vc⇣2 s, λs. (bval b s --> wp⇣1 s) ∧ (¬bval b s --> wp⇣2 s)))" |"vcpre (Awhile I b c) Q =  (let (vcc,wpc) = vcpre c I   in (λs. (I s ∧ ¬ bval b s --> Q s) ∧           (I s ∧ bval b s --> wpc s) ∧ vcc s, I))"lemma vcpre_vc_pre: "vcpre c Q = (vc c Q, pre c Q)"by (induct c arbitrary: Q) (simp_all add: Let_def)end`