author | nipkow |
Mon, 10 Sep 2018 15:08:56 +0200 | |
changeset 68966 | 2881f6cccc67 |
parent 68776 | 403dd13cf6e9 |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow *) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
2 |
|
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67613
diff
changeset
|
3 |
subsection "Verification Conditions for Total Correctness" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67613
diff
changeset
|
4 |
|
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67613
diff
changeset
|
5 |
subsubsection "The Standard Approach" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67613
diff
changeset
|
6 |
|
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
7 |
theory VCG_Total_EX |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
63538
diff
changeset
|
8 |
imports Hoare_Total_EX |
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
9 |
begin |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
10 |
|
67406 | 11 |
text\<open>Annotated commands: commands where loops are annotated with |
12 |
invariants.\<close> |
|
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
13 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
14 |
datatype acom = |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
15 |
Askip ("SKIP") | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
16 |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
17 |
Aseq acom acom ("_;;/ _" [60, 61] 60) | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
18 |
Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
19 |
Awhile "nat \<Rightarrow> assn" bexp acom |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
20 |
("({_}/ WHILE _/ DO _)" [0, 0, 61] 61) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
21 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
22 |
notation com.SKIP ("SKIP") |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
23 |
|
67406 | 24 |
text\<open>Strip annotations:\<close> |
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
25 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
26 |
fun strip :: "acom \<Rightarrow> com" where |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
27 |
"strip SKIP = SKIP" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
28 |
"strip (x ::= a) = (x ::= a)" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
29 |
"strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
30 |
"strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
31 |
"strip ({_} WHILE b DO C) = (WHILE b DO strip C)" |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
32 |
|
67406 | 33 |
text\<open>Weakest precondition from annotated commands:\<close> |
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
34 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
35 |
fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
36 |
"pre SKIP Q = Q" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
37 |
"pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
38 |
"pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
39 |
"pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
40 |
(\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" | |
67613 | 41 |
"pre ({I} WHILE b DO C) Q = (\<lambda>s. \<exists>n. I n s)" |
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
42 |
|
67406 | 43 |
text\<open>Verification condition:\<close> |
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
44 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
45 |
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
46 |
"vc SKIP Q = True" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
47 |
"vc (x ::= a) Q = True" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
48 |
"vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
49 |
"vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" | |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
50 |
"vc ({I} WHILE b DO C) Q = |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
51 |
(\<forall>s n. (I (Suc n) s \<longrightarrow> pre C (I n) s) \<and> |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
52 |
(I (Suc n) s \<longrightarrow> bval b s) \<and> |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
53 |
(I 0 s \<longrightarrow> \<not> bval b s \<and> Q s) \<and> |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
54 |
vc C (I n))" |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
55 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
56 |
lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}" |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
57 |
proof(induction C arbitrary: Q) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
58 |
case (Awhile I b C) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
59 |
show ?case |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
60 |
proof(simp, rule conseq[OF _ While[of I]], goal_cases) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
61 |
case (2 n) show ?case |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
62 |
using Awhile.IH[of "I n"] Awhile.prems |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
63 |
by (auto intro: strengthen_pre) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
64 |
qed (insert Awhile.prems, auto) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
65 |
qed (auto intro: conseq Seq If simp: Skip Assign) |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
66 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
67 |
text\<open>When trying to extend the completeness proof of the VCG for partial correctness |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
68 |
to total correctness one runs into the following problem. |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
69 |
In the case of the while-rule, the universally quantified \<open>n\<close> in the first premise |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
70 |
means that for that premise the induction hypothesis does not yield a single |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
71 |
annotated command \<open>C\<close> but merely that for every \<open>n\<close> such a \<open>C\<close> exists.\<close> |
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
72 |
|
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
diff
changeset
|
73 |
end |