35 (\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" | |
35 (\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" | |
36 "pre ({I} WHILE b DO C) Q = I" |
36 "pre ({I} WHILE b DO C) Q = I" |
37 |
37 |
38 text{* Verification condition: *} |
38 text{* Verification condition: *} |
39 |
39 |
40 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
40 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where |
41 "vc SKIP Q = (\<lambda>s. True)" | |
41 "vc SKIP Q = True" | |
42 "vc (x ::= a) Q = (\<lambda>s. True)" | |
42 "vc (x ::= a) Q = True" | |
43 "vc (C\<^sub>1;; C\<^sub>2) Q = (\<lambda>s. vc C\<^sub>1 (pre C\<^sub>2 Q) s \<and> vc C\<^sub>2 Q s)" | |
43 "vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" | |
44 "vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (\<lambda>s. vc C\<^sub>1 Q s \<and> vc C\<^sub>2 Q s)" | |
44 "vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" | |
45 "vc ({I} WHILE b DO C) Q = |
45 "vc ({I} WHILE b DO C) Q = |
46 (\<lambda>s. (I s \<and> bval b s \<longrightarrow> pre C I s) \<and> |
46 ((\<forall>s. (I s \<and> bval b s \<longrightarrow> pre C I s) \<and> |
47 (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> |
47 (I s \<and> \<not> bval b s \<longrightarrow> Q s)) \<and> |
48 vc C I s)" |
48 vc C I)" |
49 |
49 |
50 |
50 |
51 text {* Soundness: *} |
51 text {* Soundness: *} |
52 |
52 |
53 lemma vc_sound: "\<forall>s. vc C Q s \<Longrightarrow> \<turnstile> {pre C Q} strip C {Q}" |
53 lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile> {pre C Q} strip C {Q}" |
54 proof(induction C arbitrary: Q) |
54 proof(induction C arbitrary: Q) |
55 case (Awhile I b C) |
55 case (Awhile I b C) |
56 show ?case |
56 show ?case |
57 proof(simp, rule While') |
57 proof(simp, rule While') |
58 from `\<forall>s. vc (Awhile I b C) Q s` |
58 from `vc (Awhile I b C) Q` |
59 have vc: "\<forall>s. vc C I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and |
59 have vc: "vc C I" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and |
60 pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre C I s" by simp_all |
60 pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre C I s" by simp_all |
61 have "\<turnstile> {pre C I} strip C {I}" by(rule Awhile.IH[OF vc]) |
61 have "\<turnstile> {pre C I} strip C {I}" by(rule Awhile.IH[OF vc]) |
62 with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}" |
62 with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}" |
63 by(rule strengthen_pre) |
63 by(rule strengthen_pre) |
64 show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
64 show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
65 qed |
65 qed |
66 qed (auto intro: hoare.conseq) |
66 qed (auto intro: hoare.conseq) |
67 |
67 |
68 corollary vc_sound': |
68 corollary vc_sound': |
69 "\<lbrakk> \<forall>s. vc C Q s; \<forall>s. P s \<longrightarrow> pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}" |
69 "\<lbrakk> vc C Q; \<forall>s. P s \<longrightarrow> pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}" |
70 by (metis strengthen_pre vc_sound) |
70 by (metis strengthen_pre vc_sound) |
71 |
71 |
72 |
72 |
73 text{* Completeness: *} |
73 text{* Completeness: *} |
74 |
74 |
77 proof (induction C arbitrary: P P' s) |
77 proof (induction C arbitrary: P P' s) |
78 case Aseq thus ?case by simp metis |
78 case Aseq thus ?case by simp metis |
79 qed simp_all |
79 qed simp_all |
80 |
80 |
81 lemma vc_mono: |
81 lemma vc_mono: |
82 "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc C P s \<Longrightarrow> vc C P' s" |
82 "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc C P \<Longrightarrow> vc C P'" |
83 proof(induction C arbitrary: P P') |
83 proof(induction C arbitrary: P P') |
84 case Aseq thus ?case by simp (metis pre_mono) |
84 case Aseq thus ?case by simp (metis pre_mono) |
85 qed simp_all |
85 qed simp_all |
86 |
86 |
87 lemma vc_complete: |
87 lemma vc_complete: |
88 "\<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 "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>C. strip C = c \<and> vc C Q \<and> (\<forall>s. P s \<longrightarrow> pre C Q s)" |
89 (is "_ \<Longrightarrow> \<exists>C. ?G P c Q C") |
89 (is "_ \<Longrightarrow> \<exists>C. ?G P c Q C") |
90 proof (induction rule: hoare.induct) |
90 proof (induction rule: hoare.induct) |
91 case Skip |
91 case Skip |
92 show ?case (is "\<exists>C. ?C C") |
92 show ?case (is "\<exists>C. ?C C") |
93 proof show "?C Askip" by simp qed |
93 proof show "?C Askip" by simp qed |