Quelle  VCG_Total_EX.thy

(* Author: Tobias Nipkow *)

subsection "Verification Conditions for Total Correctness"

subsubsection "The Standard Approach"

theory VCG_Total_EX
imports Hoare_Total_EX
begin

text‹Annotated commands: commands where loops are annotated with
 invariants.›

datatype acom =
  Askip                  (‹SKIP›) |
  Aassign vname aexp     (‹(_ ::= _)› [1000, 61] 61) |
  Aseq   acom acom       (‹_;;/ _›  [60, 61] 60) |
  Aif bexp acom acom     (‹(IF _/ THEN _/ ELSE _)›  [0, 0, 61] 61) |
  Awhile "nat ==> 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 = (λs. ∃n. I n s)"

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 n. (I (Suc n) s ⟶ pre C (I n) s) ∧
       (I (Suc n) s ⟶ bval b s) ∧
       (I 0 s ⟶ ¬ bval b s ∧ Q s) ∧
       vc C (I n))"

lemma vc_sound: "vc C Q ==> ⊨🪙t {pre C Q} strip C {Q}"
proof(induction C arbitrary: Q)
  case (Awhile I b C)
  show ?case
  proof(simp, rule conseq[OF _ While[of I]], goal_cases)
    case (2 n) show ?case
      using Awhile.IH[of "I n"] Awhile.prems
      by (auto intro: strengthen_pre)
  qed (insert Awhile.prems, auto)
qed (auto intro: conseq Seq If simp: Skip Assign)

text‹When trying to extend the completeness proof of the VCG for partial correctness
 to total correctness one runs into the following problem.
 In the case of the while-rule, the universally quantified ‹n› i
means that for that premise the induction hypothesis does not yield a single
annotated command ‹C› but merely that for every ‹n› such a ‹C› exists.›

end