|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory VCG_Total_EX |
|
4 imports "~~/src/HOL/IMP/Hoare_Total_EX" |
|
5 begin |
|
6 |
|
7 subsection "Verification Conditions for Total Correctness" |
|
8 |
|
9 text{* Annotated commands: commands where loops are annotated with |
|
10 invariants. *} |
|
11 |
|
12 datatype acom = |
|
13 Askip ("SKIP") | |
|
14 Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | |
|
15 Aseq acom acom ("_;;/ _" [60, 61] 60) | |
|
16 Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | |
|
17 Awhile "nat \<Rightarrow> assn" bexp acom |
|
18 ("({_}/ WHILE _/ DO _)" [0, 0, 61] 61) |
|
19 |
|
20 notation com.SKIP ("SKIP") |
|
21 |
|
22 text{* Strip annotations: *} |
|
23 |
|
24 fun strip :: "acom \<Rightarrow> com" where |
|
25 "strip SKIP = SKIP" | |
|
26 "strip (x ::= a) = (x ::= a)" | |
|
27 "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" | |
|
28 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" | |
|
29 "strip ({_} WHILE b DO C) = (WHILE b DO strip C)" |
|
30 |
|
31 text{* Weakest precondition from annotated commands: *} |
|
32 |
|
33 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
|
34 "pre SKIP Q = Q" | |
|
35 "pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
|
36 "pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" | |
|
37 "pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = |
|
38 (\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" | |
|
39 "pre ({I} WHILE b DO C) Q = (\<lambda>s. EX n. I n s)" |
|
40 |
|
41 text{* Verification condition: *} |
|
42 |
|
43 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where |
|
44 "vc SKIP Q = True" | |
|
45 "vc (x ::= a) Q = True" | |
|
46 "vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" | |
|
47 "vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" | |
|
48 "vc ({I} WHILE b DO C) Q = |
|
49 (\<forall>s n. (I (Suc n) s \<longrightarrow> pre C (I n) s) \<and> |
|
50 (I (Suc n) s \<longrightarrow> bval b s) \<and> |
|
51 (I 0 s \<longrightarrow> \<not> bval b s \<and> Q s) \<and> |
|
52 vc C (I n))" |
|
53 |
|
54 lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}" |
|
55 proof(induction C arbitrary: Q) |
|
56 case (Awhile I b C) |
|
57 show ?case |
|
58 proof(simp, rule conseq[OF _ While[of I]], goal_cases) |
|
59 case (2 n) show ?case |
|
60 using Awhile.IH[of "I n"] Awhile.prems |
|
61 by (auto intro: strengthen_pre) |
|
62 qed (insert Awhile.prems, auto) |
|
63 qed (auto intro: conseq Seq If simp: Skip Assign) |
|
64 |
|
65 text\<open>When trying to extend the completeness proof of the VCG for partial correctness |
|
66 to total correctness one runs into the following problem. |
|
67 In the case of the while-rule, the universally quantified \<open>n\<close> in the first premise |
|
68 means that for that premise the induction hypothesis does not yield a single |
|
69 annotated command \<open>C\<close> but merely that for every \<open>n\<close> such a \<open>C\<close> exists.\<close> |
|
70 |
|
71 end |