|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Hoare_Total_EX imports Hoare_Sound_Complete Hoare_Examples begin |
|
4 |
|
5 subsection "Hoare Logic for Total Correctness" |
|
6 |
|
7 text{* This is the standard set of rules that you find in many publications. |
|
8 The While-rule is different from the one in Concrete Semantics in that the |
|
9 invariant is indexed by natural numbers and goes down by 1 with |
|
10 every iteration. The completeness proof is easier but the rule is harder |
|
11 to apply in program proofs. *} |
|
12 |
|
13 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
|
14 ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
|
15 "\<Turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))" |
|
16 |
|
17 inductive |
|
18 hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) |
|
19 where |
|
20 |
|
21 Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" | |
|
22 |
|
23 Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" | |
|
24 |
|
25 Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" | |
|
26 |
|
27 If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk> |
|
28 \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | |
|
29 |
|
30 While: |
|
31 "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {P (Suc n)} c {P n}; |
|
32 \<forall>n s. P (Suc n) s \<longrightarrow> bval b s; \<forall>s. P 0 s \<longrightarrow> \<not> bval b s \<rbrakk> |
|
33 \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. \<exists>n. P n s} WHILE b DO c {P 0}" | |
|
34 |
|
35 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> |
|
36 \<turnstile>\<^sub>t {P'}c{Q'}" |
|
37 |
|
38 text{* Building in the consequence rule: *} |
|
39 |
|
40 lemma strengthen_pre: |
|
41 "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}" |
|
42 by (metis conseq) |
|
43 |
|
44 lemma weaken_post: |
|
45 "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}" |
|
46 by (metis conseq) |
|
47 |
|
48 lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}" |
|
49 by (simp add: strengthen_pre[OF _ Assign]) |
|
50 |
|
51 text{* The soundness theorem: *} |
|
52 |
|
53 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
|
54 proof(unfold hoare_tvalid_def, induction rule: hoaret.induct) |
|
55 case (While P c b) |
|
56 { |
|
57 fix n s |
|
58 have "\<lbrakk> P n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t" |
|
59 proof(induction "n" arbitrary: s) |
|
60 case 0 thus ?case using While.hyps(3) WhileFalse by blast |
|
61 next |
|
62 case (Suc n) |
|
63 thus ?case by (meson While.IH While.hyps(2) WhileTrue) |
|
64 qed |
|
65 } |
|
66 thus ?case by auto |
|
67 next |
|
68 case If thus ?case by auto blast |
|
69 qed fastforce+ |
|
70 |
|
71 |
|
72 definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where |
|
73 "wp\<^sub>t c Q = (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
|
74 |
|
75 lemma [simp]: "wp\<^sub>t SKIP Q = Q" |
|
76 by(auto intro!: ext simp: wpt_def) |
|
77 |
|
78 lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))" |
|
79 by(auto intro!: ext simp: wpt_def) |
|
80 |
|
81 lemma [simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)" |
|
82 unfolding wpt_def |
|
83 apply(rule ext) |
|
84 apply auto |
|
85 done |
|
86 |
|
87 lemma [simp]: |
|
88 "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)" |
|
89 apply(unfold wpt_def) |
|
90 apply(rule ext) |
|
91 apply auto |
|
92 done |
|
93 |
|
94 |
|
95 text{* Function @{text wpw} computes the weakest precondition of a While-loop |
|
96 that is unfolded a fixed number of times. *} |
|
97 |
|
98 fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn \<Rightarrow> assn" where |
|
99 "wpw b c 0 Q s = (\<not> bval b s \<and> Q s)" | |
|
100 "wpw b c (Suc n) Q s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and> wpw b c n Q s'))" |
|
101 |
|
102 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q t \<Longrightarrow> \<exists>n. wpw b c n Q s" |
|
103 proof(induction "WHILE b DO c" s t rule: big_step_induct) |
|
104 case WhileFalse thus ?case using wpw.simps(1) by blast |
|
105 next |
|
106 case WhileTrue thus ?case using wpw.simps(2) by blast |
|
107 qed |
|
108 |
|
109 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
|
110 proof (induction c arbitrary: Q) |
|
111 case SKIP show ?case by (auto intro:hoaret.Skip) |
|
112 next |
|
113 case Assign show ?case by (auto intro:hoaret.Assign) |
|
114 next |
|
115 case Seq thus ?case by (auto intro:hoaret.Seq) |
|
116 next |
|
117 case If thus ?case by (auto intro:hoaret.If hoaret.conseq) |
|
118 next |
|
119 case (While b c) |
|
120 let ?w = "WHILE b DO c" |
|
121 have c1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> (\<exists>n. wpw b c n Q s)" |
|
122 unfolding wpt_def by (metis WHILE_Its) |
|
123 have c3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> Q s" by simp |
|
124 have w2: "\<forall>n s. wpw b c (Suc n) Q s \<longrightarrow> bval b s" by simp |
|
125 have w3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> \<not> bval b s" by simp |
|
126 { fix n |
|
127 have 1: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)" |
|
128 by simp |
|
129 note strengthen_pre[OF 1 While.IH[of "wpw b c n Q", unfolded wpt_def]] |
|
130 } |
|
131 from conseq[OF c1 hoaret.While[OF this w2 w3] c3] |
|
132 show ?case . |
|
133 qed |
|
134 |
|
135 theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}" |
|
136 apply(rule strengthen_pre[OF _ wpt_is_pre]) |
|
137 apply(auto simp: hoare_tvalid_def wpt_def) |
|
138 done |
|
139 |
|
140 corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
|
141 by (metis hoaret_sound hoaret_complete) |
|
142 |
|
143 end |