|
1 header{* Hoare Logic for Total Correctness *} |
|
2 |
|
3 theory HoareT imports Hoare_Sound_Complete Util begin |
|
4 |
|
5 text{* |
|
6 Now that we have termination, we can define |
|
7 total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*} |
|
8 |
|
9 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
|
10 ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
|
11 "\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
|
12 |
|
13 text{* Proveability of Hoare triples in the proof system for total |
|
14 correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined |
|
15 inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for |
|
16 @{text"\<turnstile>"} only in the one place where nontermination can arise: the |
|
17 @{term While}-rule. *} |
|
18 |
|
19 inductive |
|
20 hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) |
|
21 where |
|
22 Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" | |
|
23 Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" | |
|
24 Semi: "\<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}" | |
|
25 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> |
|
26 \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" | |
|
27 While: |
|
28 "\<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> |
|
29 \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" | |
|
30 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> |
|
31 \<turnstile>\<^sub>t {P'}c{Q'}" |
|
32 |
|
33 text{* The @{term While}-rule is like the one for partial correctness but it |
|
34 requires additionally that with every execution of the loop body some measure |
|
35 function @{term[source]"f :: state \<Rightarrow> nat"} decreases. *} |
|
36 |
|
37 lemma strengthen_pre: |
|
38 "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}" |
|
39 by (metis conseq) |
|
40 |
|
41 lemma weaken_post: |
|
42 "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}" |
|
43 by (metis conseq) |
|
44 |
|
45 lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}" |
|
46 by (simp add: strengthen_pre[OF _ Assign]) |
|
47 |
|
48 lemma While': |
|
49 assumes "\<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}" |
|
50 and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s" |
|
51 shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}" |
|
52 by(blast intro: assms(1) weaken_post[OF While assms(2)]) |
|
53 |
|
54 text{* Our standard example: *} |
|
55 |
|
56 abbreviation "w n == |
|
57 WHILE Less (V ''y'') (N n) |
|
58 DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )" |
|
59 |
|
60 lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}" |
|
61 apply(rule Semi) |
|
62 prefer 2 |
|
63 apply(rule While' |
|
64 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 <= n \<and> 0 <= s ''y'' \<and> s ''y'' \<le> n" |
|
65 and f = "\<lambda>s. nat n - nat (s ''y'')"]) |
|
66 apply(rule Semi) |
|
67 prefer 2 |
|
68 apply(rule Assign) |
|
69 apply(rule Assign') |
|
70 apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps) |
|
71 apply clarsimp |
|
72 apply arith |
|
73 apply fastsimp |
|
74 apply(rule Semi) |
|
75 prefer 2 |
|
76 apply(rule Assign) |
|
77 apply(rule Assign') |
|
78 apply simp |
|
79 done |
|
80 |
|
81 |
|
82 text{* The soundness theorem: *} |
|
83 |
|
84 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
|
85 proof(unfold hoare_tvalid_def, induct rule: hoaret.induct) |
|
86 case (While P b f c) |
|
87 show ?case |
|
88 proof |
|
89 fix s |
|
90 show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)" |
|
91 proof(induct "f s" arbitrary: s rule: less_induct) |
|
92 case (less n) |
|
93 thus ?case by (metis While(2) WhileFalse WhileTrue) |
|
94 qed |
|
95 qed |
|
96 next |
|
97 case If thus ?case by auto blast |
|
98 qed fastsimp+ |
|
99 |
|
100 |
|
101 text{* |
|
102 The completeness proof proceeds along the same lines as the one for partial |
|
103 correctness. First we have to strengthen our notion of weakest precondition |
|
104 to take termination into account: *} |
|
105 |
|
106 definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where |
|
107 "wp\<^sub>t c Q \<equiv> \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t" |
|
108 |
|
109 lemma [simp]: "wp\<^sub>t SKIP Q = Q" |
|
110 by(auto intro!: ext simp: wpt_def) |
|
111 |
|
112 lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))" |
|
113 by(auto intro!: ext simp: wpt_def) |
|
114 |
|
115 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)" |
|
116 unfolding wpt_def |
|
117 apply(rule ext) |
|
118 apply auto |
|
119 done |
|
120 |
|
121 lemma [simp]: |
|
122 "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)" |
|
123 apply(unfold wpt_def) |
|
124 apply(rule ext) |
|
125 apply auto |
|
126 done |
|
127 |
|
128 |
|
129 text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to |
|
130 terminate when started in state @{text s}. Because this is a truly partial |
|
131 function, we define it as an (inductive) relation first: *} |
|
132 |
|
133 inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where |
|
134 Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" | |
|
135 Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)" |
|
136 |
|
137 text{* The relation is in fact a function: *} |
|
138 |
|
139 lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'" |
|
140 proof(induct arbitrary: n' rule:Its.induct) |
|
141 (* new release: |
|
142 case Its_0 thus ?case by(metis Its.cases) |
|
143 next |
|
144 case Its_Suc thus ?case by(metis Its.cases big_step_determ) |
|
145 qed |
|
146 *) |
|
147 case Its_0 |
|
148 from this(1) Its.cases[OF this(2)] show ?case by metis |
|
149 next |
|
150 case (Its_Suc b s c s' n n') |
|
151 note C = this |
|
152 from this(5) show ?case |
|
153 proof cases |
|
154 case Its_0 with Its_Suc(1) show ?thesis by blast |
|
155 next |
|
156 case Its_Suc with C show ?thesis by(metis big_step_determ) |
|
157 qed |
|
158 qed |
|
159 |
|
160 text{* For all terminating loops, @{const Its} yields a result: *} |
|
161 |
|
162 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n" |
|
163 proof(induct "WHILE b DO c" s t rule: big_step_induct) |
|
164 case WhileFalse thus ?case by (metis Its_0) |
|
165 next |
|
166 case WhileTrue thus ?case by (metis Its_Suc) |
|
167 qed |
|
168 |
|
169 text{* Now the relation is turned into a function with the help of |
|
170 the description operator @{text THE}: *} |
|
171 |
|
172 definition its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat" where |
|
173 "its b c s = (THE n. Its b c s n)" |
|
174 |
|
175 text{* The key property: every loop iteration increases @{const its} by 1. *} |
|
176 |
|
177 lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk> |
|
178 \<Longrightarrow> its b c s = Suc(its b c s')" |
|
179 by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality) |
|
180 |
|
181 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
|
182 proof (induct c arbitrary: Q) |
|
183 case SKIP show ?case by simp (blast intro:hoaret.Skip) |
|
184 next |
|
185 case Assign show ?case by simp (blast intro:hoaret.Assign) |
|
186 next |
|
187 case Semi thus ?case by simp (blast intro:hoaret.Semi) |
|
188 next |
|
189 case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq) |
|
190 next |
|
191 case (While b c) |
|
192 let ?w = "WHILE b DO c" |
|
193 { fix n |
|
194 have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> its b c s = n \<longrightarrow> |
|
195 wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> its b c s' < n) s" |
|
196 unfolding wpt_def by (metis WhileE its_Suc lessI) |
|
197 note strengthen_pre[OF this While] |
|
198 } note hoaret.While[OF this] |
|
199 moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def) |
|
200 ultimately show ?case by(rule weaken_post) |
|
201 qed |
|
202 |
|
203 |
|
204 text{*\noindent In the @{term While}-case, @{const its} provides the obvious |
|
205 termination argument. |
|
206 |
|
207 The actual completeness theorem follows directly, in the same manner |
|
208 as for partial correctness: *} |
|
209 |
|
210 theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}" |
|
211 apply(rule strengthen_pre[OF _ wpt_is_pre]) |
|
212 apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def) |
|
213 done |
|
214 |
|
215 end |