18 text{* Strip annotations: *} |
18 text{* Strip annotations: *} |
19 |
19 |
20 fun strip :: "acom \<Rightarrow> com" where |
20 fun strip :: "acom \<Rightarrow> com" where |
21 "strip SKIP = com.SKIP" | |
21 "strip SKIP = com.SKIP" | |
22 "strip (x ::= a) = (x ::= a)" | |
22 "strip (x ::= a) = (x ::= a)" | |
23 "strip (c\<^isub>1;; c\<^isub>2) = (strip c\<^isub>1;; strip c\<^isub>2)" | |
23 "strip (C\<^isub>1;; C\<^isub>2) = (strip C\<^isub>1;; strip C\<^isub>2)" | |
24 "strip (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" | |
24 "strip (IF b THEN C\<^isub>1 ELSE C\<^isub>2) = (IF b THEN strip C\<^isub>1 ELSE strip C\<^isub>2)" | |
25 "strip ({_} WHILE b DO c) = (WHILE b DO strip c)" |
25 "strip ({_} WHILE b DO C) = (WHILE b DO strip C)" |
26 |
26 |
27 text{* Weakest precondition from annotated commands: *} |
27 text{* Weakest precondition from annotated commands: *} |
28 |
28 |
29 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
29 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
30 "pre SKIP Q = Q" | |
30 "pre SKIP Q = Q" | |
31 "pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
31 "pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
32 "pre (c\<^isub>1;; c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" | |
32 "pre (C\<^isub>1;; C\<^isub>2) Q = pre C\<^isub>1 (pre C\<^isub>2 Q)" | |
33 "pre (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = |
33 "pre (IF b THEN C\<^isub>1 ELSE C\<^isub>2) Q = |
34 (\<lambda>s. if bval b s then pre c\<^isub>1 Q s else pre c\<^isub>2 Q s)" | |
34 (\<lambda>s. if bval b s then pre C\<^isub>1 Q s else pre C\<^isub>2 Q s)" | |
35 "pre ({I} WHILE b DO c) Q = I" |
35 "pre ({I} WHILE b DO C) Q = I" |
36 |
36 |
37 text{* Verification condition: *} |
37 text{* Verification condition: *} |
38 |
38 |
39 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
39 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
40 "vc SKIP Q = (\<lambda>s. True)" | |
40 "vc SKIP Q = (\<lambda>s. True)" | |
41 "vc (x ::= a) Q = (\<lambda>s. True)" | |
41 "vc (x ::= a) Q = (\<lambda>s. True)" | |
42 "vc (c\<^isub>1;; c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" | |
42 "vc (C\<^isub>1;; C\<^isub>2) Q = (\<lambda>s. vc C\<^isub>1 (pre C\<^isub>2 Q) s \<and> vc C\<^isub>2 Q s)" | |
43 "vc (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" | |
43 "vc (IF b THEN C\<^isub>1 ELSE C\<^isub>2) Q = (\<lambda>s. vc C\<^isub>1 Q s \<and> vc C\<^isub>2 Q s)" | |
44 "vc ({I} WHILE b DO c) Q = |
44 "vc ({I} WHILE b DO C) Q = |
45 (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> |
45 (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> |
46 (I s \<and> bval b s \<longrightarrow> pre c I s) \<and> |
46 (I s \<and> bval b s \<longrightarrow> pre C I s) \<and> |
47 vc c I s)" |
47 vc C I s)" |
48 |
48 |
49 |
49 |
50 text {* Soundness: *} |
50 text {* Soundness: *} |
51 |
51 |
52 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}" |
52 lemma vc_sound: "\<forall>s. vc C Q s \<Longrightarrow> \<turnstile> {pre C Q} strip C {Q}" |
53 proof(induction c arbitrary: Q) |
53 proof(induction C arbitrary: Q) |
54 case (Awhile I b c) |
54 case (Awhile I b C) |
55 show ?case |
55 show ?case |
56 proof(simp, rule While') |
56 proof(simp, rule While') |
57 from `\<forall>s. vc (Awhile I b c) Q s` |
57 from `\<forall>s. vc (Awhile I b C) Q s` |
58 have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and |
58 have vc: "\<forall>s. vc C I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and |
59 pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all |
59 pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre C I s" by simp_all |
60 have "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc]) |
60 have "\<turnstile> {pre C I} strip C {I}" by(rule Awhile.IH[OF vc]) |
61 with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip c {I}" |
61 with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}" |
62 by(rule strengthen_pre) |
62 by(rule strengthen_pre) |
63 show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
63 show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
64 qed |
64 qed |
65 qed (auto intro: hoare.conseq) |
65 qed (auto intro: hoare.conseq) |
66 |
66 |
67 corollary vc_sound': |
67 corollary vc_sound': |
68 "\<lbrakk> \<forall>s. vc c Q s; \<forall>s. P s \<longrightarrow> pre c Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip c {Q}" |
68 "\<lbrakk> \<forall>s. vc C Q s; \<forall>s. P s \<longrightarrow> pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}" |
69 by (metis strengthen_pre vc_sound) |
69 by (metis strengthen_pre vc_sound) |
70 |
70 |
71 |
71 |
72 text{* Completeness: *} |
72 text{* Completeness: *} |
73 |
73 |
74 lemma pre_mono: |
74 lemma pre_mono: |
75 "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s" |
75 "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre C P s \<Longrightarrow> pre C P' s" |
76 proof (induction c arbitrary: P P' s) |
76 proof (induction C arbitrary: P P' s) |
77 case Aseq thus ?case by simp metis |
77 case Aseq thus ?case by simp metis |
78 qed simp_all |
78 qed simp_all |
79 |
79 |
80 lemma vc_mono: |
80 lemma vc_mono: |
81 "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s" |
81 "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc C P s \<Longrightarrow> vc C P' s" |
82 proof(induction c arbitrary: P P') |
82 proof(induction C arbitrary: P P') |
83 case Aseq thus ?case by simp (metis pre_mono) |
83 case Aseq thus ?case by simp (metis pre_mono) |
84 qed simp_all |
84 qed simp_all |
85 |
85 |
86 lemma vc_complete: |
86 lemma vc_complete: |
87 "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. strip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)" |
87 "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>C. strip C = c \<and> (\<forall>s. vc C Q s) \<and> (\<forall>s. P s \<longrightarrow> pre C Q s)" |
88 (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'") |
88 (is "_ \<Longrightarrow> \<exists>C. ?G P c Q C") |
89 proof (induction rule: hoare.induct) |
89 proof (induction rule: hoare.induct) |
90 case Skip |
90 case Skip |
91 show ?case (is "\<exists>ac. ?C ac") |
91 show ?case (is "\<exists>C. ?C C") |
92 proof show "?C Askip" by simp qed |
92 proof show "?C Askip" by simp qed |
93 next |
93 next |
94 case (Assign P a x) |
94 case (Assign P a x) |
95 show ?case (is "\<exists>ac. ?C ac") |
95 show ?case (is "\<exists>C. ?C C") |
96 proof show "?C(Aassign x a)" by simp qed |
96 proof show "?C(Aassign x a)" by simp qed |
97 next |
97 next |
98 case (Seq P c1 Q c2 R) |
98 case (Seq P c1 Q c2 R) |
99 from Seq.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast |
99 from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast |
100 from Seq.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast |
100 from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast |
101 show ?case (is "\<exists>ac. ?C ac") |
101 show ?case (is "\<exists>C. ?C C") |
102 proof |
102 proof |
103 show "?C(Aseq ac1 ac2)" |
103 show "?C(Aseq C1 C2)" |
104 using ih1 ih2 by (fastforce elim!: pre_mono vc_mono) |
104 using ih1 ih2 by (fastforce elim!: pre_mono vc_mono) |
105 qed |
105 qed |
106 next |
106 next |
107 case (If P b c1 Q c2) |
107 case (If P b c1 Q c2) |
108 from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1" |
108 from If.IH obtain C1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q C1" |
109 by blast |
109 by blast |
110 from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2" |
110 from If.IH obtain C2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q C2" |
111 by blast |
111 by blast |
112 show ?case (is "\<exists>ac. ?C ac") |
112 show ?case (is "\<exists>C. ?C C") |
113 proof |
113 proof |
114 show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp |
114 show "?C(Aif b C1 C2)" using ih1 ih2 by simp |
115 qed |
115 qed |
116 next |
116 next |
117 case (While P b c) |
117 case (While P b c) |
118 from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast |
118 from While.IH obtain C where ih: "?G (\<lambda>s. P s \<and> bval b s) c P C" by blast |
119 show ?case (is "\<exists>ac. ?C ac") |
119 show ?case (is "\<exists>C. ?C C") |
120 proof show "?C(Awhile P b ac)" using ih by simp qed |
120 proof show "?C(Awhile P b C)" using ih by simp qed |
121 next |
121 next |
122 case conseq thus ?case by(fast elim!: pre_mono vc_mono) |
122 case conseq thus ?case by(fast elim!: pre_mono vc_mono) |
123 qed |
123 qed |
124 |
124 |
125 end |
125 end |