author | nipkow |
Thu, 30 May 2013 08:27:51 +0200 | |
changeset 52228 | ee8e3eaad24c |
parent 52227 | f9e68ba3f004 |
child 52281 | 780b3870319f |
permissions | -rw-r--r-- |
50421 | 1 |
(* Author: Tobias Nipkow *) |
43158 | 2 |
|
52228 | 3 |
theory HoareT imports Hoare_Sound_Complete Hoare_Examples begin |
43158 | 4 |
|
50421 | 5 |
subsection "Hoare Logic for Total Correctness" |
6 |
||
46203 | 7 |
text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only |
8 |
works if execution is deterministic (which it is in our case). *} |
|
43158 | 9 |
|
10 |
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
|
11 |
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
|
12 |
"\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
|
13 |
||
45114 | 14 |
text{* Provability of Hoare triples in the proof system for total |
43158 | 15 |
correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined |
16 |
inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for |
|
17 |
@{text"\<turnstile>"} only in the one place where nontermination can arise: the |
|
18 |
@{term While}-rule. *} |
|
19 |
||
20 |
inductive |
|
21 |
hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) |
|
22 |
where |
|
23 |
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" | |
|
24 |
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" | |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
50421
diff
changeset
|
25 |
Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;;c\<^isub>2 {P\<^isub>3}" | |
43158 | 26 |
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk> |
27 |
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" | |
|
28 |
While: |
|
52228 | 29 |
"\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'. T s n' \<and> n' < n)} \<rbrakk> |
30 |
\<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" | |
|
43158 | 31 |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> |
32 |
\<turnstile>\<^sub>t {P'}c{Q'}" |
|
33 |
||
34 |
text{* The @{term While}-rule is like the one for partial correctness but it |
|
35 |
requires additionally that with every execution of the loop body some measure |
|
36 |
function @{term[source]"f :: state \<Rightarrow> nat"} decreases. *} |
|
37 |
||
38 |
lemma strengthen_pre: |
|
39 |
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}" |
|
40 |
by (metis conseq) |
|
41 |
||
42 |
lemma weaken_post: |
|
43 |
"\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}" |
|
44 |
by (metis conseq) |
|
45 |
||
46 |
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}" |
|
47 |
by (simp add: strengthen_pre[OF _ Assign]) |
|
48 |
||
49 |
lemma While': |
|
52228 | 50 |
assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'. T s n' \<and> n' < n)}" |
43158 | 51 |
and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s" |
52228 | 52 |
shows "\<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {Q}" |
43158 | 53 |
by(blast intro: assms(1) weaken_post[OF While assms(2)]) |
54 |
||
52227 | 55 |
lemma While_fun: |
56 |
"\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk> |
|
57 |
\<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
|
52228 | 58 |
by (rule While [where T="\<lambda>s n. f s = n", simplified]) |
52227 | 59 |
|
43158 | 60 |
text{* Our standard example: *} |
61 |
||
52228 | 62 |
lemma "\<turnstile>\<^sub>t {\<lambda>s. s ''x'' = i} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum i}" |
47818 | 63 |
apply(rule Seq) |
52228 | 64 |
prefer 2 |
65 |
apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum i - sum(s ''x''))" |
|
66 |
and T = "\<lambda>s n. n = nat(s ''x'')"]) |
|
67 |
apply(rule Seq) |
|
68 |
prefer 2 |
|
69 |
apply(rule Assign) |
|
70 |
apply(rule Assign') |
|
71 |
apply simp |
|
72 |
apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps) |
|
73 |
apply(simp) |
|
43158 | 74 |
apply(rule Assign') |
75 |
apply simp |
|
76 |
done |
|
77 |
||
78 |
||
79 |
text{* The soundness theorem: *} |
|
80 |
||
81 |
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
|
82 |
proof(unfold hoare_tvalid_def, induct rule: hoaret.induct) |
|
52227 | 83 |
case (While P b T c) |
84 |
{ |
|
85 |
fix s n |
|
52228 | 86 |
have "\<lbrakk> P s; T s n \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t" |
52227 | 87 |
proof(induction "n" arbitrary: s rule: less_induct) |
43158 | 88 |
case (less n) |
89 |
thus ?case by (metis While(2) WhileFalse WhileTrue) |
|
90 |
qed |
|
52227 | 91 |
} |
92 |
thus ?case by auto |
|
43158 | 93 |
next |
94 |
case If thus ?case by auto blast |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44177
diff
changeset
|
95 |
qed fastforce+ |
43158 | 96 |
|
97 |
||
98 |
text{* |
|
99 |
The completeness proof proceeds along the same lines as the one for partial |
|
100 |
correctness. First we have to strengthen our notion of weakest precondition |
|
101 |
to take termination into account: *} |
|
102 |
||
103 |
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where |
|
104 |
"wp\<^sub>t c Q \<equiv> \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t" |
|
105 |
||
106 |
lemma [simp]: "wp\<^sub>t SKIP Q = Q" |
|
107 |
by(auto intro!: ext simp: wpt_def) |
|
108 |
||
109 |
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))" |
|
110 |
by(auto intro!: ext simp: wpt_def) |
|
111 |
||
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
50421
diff
changeset
|
112 |
lemma [simp]: "wp\<^sub>t (c\<^isub>1;;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)" |
43158 | 113 |
unfolding wpt_def |
114 |
apply(rule ext) |
|
115 |
apply auto |
|
116 |
done |
|
117 |
||
118 |
lemma [simp]: |
|
119 |
"wp\<^sub>t (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^isub>1 else c\<^isub>2) Q s)" |
|
120 |
apply(unfold wpt_def) |
|
121 |
apply(rule ext) |
|
122 |
apply auto |
|
123 |
done |
|
124 |
||
125 |
||
126 |
text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to |
|
127 |
terminate when started in state @{text s}. Because this is a truly partial |
|
128 |
function, we define it as an (inductive) relation first: *} |
|
129 |
||
130 |
inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where |
|
131 |
Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" | |
|
132 |
Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)" |
|
133 |
||
134 |
text{* The relation is in fact a function: *} |
|
135 |
||
136 |
lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'" |
|
45015 | 137 |
proof(induction arbitrary: n' rule:Its.induct) |
43158 | 138 |
case Its_0 thus ?case by(metis Its.cases) |
139 |
next |
|
140 |
case Its_Suc thus ?case by(metis Its.cases big_step_determ) |
|
141 |
qed |
|
142 |
||
143 |
text{* For all terminating loops, @{const Its} yields a result: *} |
|
144 |
||
145 |
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n" |
|
45015 | 146 |
proof(induction "WHILE b DO c" s t rule: big_step_induct) |
43158 | 147 |
case WhileFalse thus ?case by (metis Its_0) |
148 |
next |
|
149 |
case WhileTrue thus ?case by (metis Its_Suc) |
|
150 |
qed |
|
151 |
||
152 |
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
|
45015 | 153 |
proof (induction c arbitrary: Q) |
43158 | 154 |
case SKIP show ?case by simp (blast intro:hoaret.Skip) |
155 |
next |
|
156 |
case Assign show ?case by simp (blast intro:hoaret.Assign) |
|
157 |
next |
|
47818 | 158 |
case Seq thus ?case by simp (blast intro:hoaret.Seq) |
43158 | 159 |
next |
160 |
case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq) |
|
161 |
next |
|
162 |
case (While b c) |
|
163 |
let ?w = "WHILE b DO c" |
|
52228 | 164 |
let ?T = "Its b c" |
52227 | 165 |
have "\<forall>s. wp\<^sub>t (WHILE b DO c) Q s \<longrightarrow> wp\<^sub>t (WHILE b DO c) Q s \<and> (\<exists>n. Its b c s n)" |
166 |
unfolding wpt_def by (metis WHILE_Its) |
|
167 |
moreover |
|
43158 | 168 |
{ fix n |
52227 | 169 |
{ fix s t |
52228 | 170 |
assume "bval b s" "?T s n" "(?w, s) \<Rightarrow> t" "Q t" |
52227 | 171 |
from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where |
172 |
"(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto |
|
52228 | 173 |
from `(?w, s') \<Rightarrow> t` obtain n'' where "?T s' n''" by (blast dest: WHILE_Its) |
52227 | 174 |
with `bval b s` `(c, s) \<Rightarrow> s'` |
52228 | 175 |
have "?T s (Suc n'')" by (rule Its_Suc) |
176 |
with `?T s n` have "n = Suc n''" by (rule Its_fun) |
|
177 |
with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T s' n''` |
|
178 |
have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s" |
|
52227 | 179 |
by (auto simp: wpt_def) |
180 |
} |
|
52228 | 181 |
hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> |
182 |
wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s" |
|
52227 | 183 |
unfolding wpt_def by auto |
184 |
(* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) |
|
43158 | 185 |
note strengthen_pre[OF this While] |
186 |
} note hoaret.While[OF this] |
|
187 |
moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def) |
|
52227 | 188 |
ultimately show ?case by (rule conseq) |
43158 | 189 |
qed |
190 |
||
191 |
||
52227 | 192 |
text{*\noindent In the @{term While}-case, @{const Its} provides the obvious |
43158 | 193 |
termination argument. |
194 |
||
195 |
The actual completeness theorem follows directly, in the same manner |
|
196 |
as for partial correctness: *} |
|
197 |
||
198 |
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}" |
|
199 |
apply(rule strengthen_pre[OF _ wpt_is_pre]) |
|
200 |
apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def) |
|
201 |
done |
|
202 |
||
203 |
end |