2 |
2 |
3 theory Hoare_Examples imports Hoare begin |
3 theory Hoare_Examples imports Hoare begin |
4 |
4 |
5 hide_const (open) sum |
5 hide_const (open) sum |
6 |
6 |
7 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
7 text\<open>Summing up the first @{text x} natural numbers in variable @{text y}.\<close> |
8 |
8 |
9 fun sum :: "int \<Rightarrow> int" where |
9 fun sum :: "int \<Rightarrow> int" where |
10 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |
10 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |
11 |
11 |
12 lemma sum_simps[simp]: |
12 lemma sum_simps[simp]: |
20 WHILE Less (N 0) (V ''x'') |
20 WHILE Less (N 0) (V ''x'') |
21 DO (''y'' ::= Plus (V ''y'') (V ''x'');; |
21 DO (''y'' ::= Plus (V ''y'') (V ''x'');; |
22 ''x'' ::= Plus (V ''x'') (N (- 1)))" |
22 ''x'' ::= Plus (V ''x'') (N (- 1)))" |
23 |
23 |
24 |
24 |
25 subsubsection{* Proof by Operational Semantics *} |
25 subsubsection\<open>Proof by Operational Semantics\<close> |
26 |
26 |
27 text{* The behaviour of the loop is proved by induction: *} |
27 text\<open>The behaviour of the loop is proved by induction:\<close> |
28 |
28 |
29 lemma while_sum: |
29 lemma while_sum: |
30 "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" |
30 "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" |
31 apply(induction wsum s t rule: big_step_induct) |
31 apply(induction wsum s t rule: big_step_induct) |
32 apply(auto) |
32 apply(auto) |
33 done |
33 done |
34 |
34 |
35 text{* We were lucky that the proof was automatic, except for the |
35 text\<open>We were lucky that the proof was automatic, except for the |
36 induction. In general, such proofs will not be so easy. The automation is |
36 induction. In general, such proofs will not be so easy. The automation is |
37 partly due to the right inversion rules that we set up as automatic |
37 partly due to the right inversion rules that we set up as automatic |
38 elimination rules that decompose big-step premises. |
38 elimination rules that decompose big-step premises. |
39 |
39 |
40 Now we prefix the loop with the necessary initialization: *} |
40 Now we prefix the loop with the necessary initialization:\<close> |
41 |
41 |
42 lemma sum_via_bigstep: |
42 lemma sum_via_bigstep: |
43 assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |
43 assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |
44 shows "t ''y'' = sum (s ''x'')" |
44 shows "t ''y'' = sum (s ''x'')" |
45 proof - |
45 proof - |
46 from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |
46 from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |
47 from while_sum[OF this] show ?thesis by simp |
47 from while_sum[OF this] show ?thesis by simp |
48 qed |
48 qed |
49 |
49 |
50 |
50 |
51 subsubsection{* Proof by Hoare Logic *} |
51 subsubsection\<open>Proof by Hoare Logic\<close> |
52 |
52 |
53 text{* Note that we deal with sequences of commands from right to left, |
53 text\<open>Note that we deal with sequences of commands from right to left, |
54 pulling back the postcondition towards the precondition. *} |
54 pulling back the postcondition towards the precondition.\<close> |
55 |
55 |
56 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" |
56 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" |
57 apply(rule Seq) |
57 apply(rule Seq) |
58 prefer 2 |
58 prefer 2 |
59 apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"]) |
59 apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"]) |
65 apply simp |
65 apply simp |
66 apply(rule Assign') |
66 apply(rule Assign') |
67 apply simp |
67 apply simp |
68 done |
68 done |
69 |
69 |
70 text{* The proof is intentionally an apply script because it merely composes |
70 text\<open>The proof is intentionally an apply script because it merely composes |
71 the rules of Hoare logic. Of course, in a few places side conditions have to |
71 the rules of Hoare logic. Of course, in a few places side conditions have to |
72 be proved. But since those proofs are 1-liners, a structured proof is |
72 be proved. But since those proofs are 1-liners, a structured proof is |
73 overkill. In fact, we shall learn later that the application of the Hoare |
73 overkill. In fact, we shall learn later that the application of the Hoare |
74 rules can be automated completely and all that is left for the user is to |
74 rules can be automated completely and all that is left for the user is to |
75 provide the loop invariants and prove the side-conditions. *} |
75 provide the loop invariants and prove the side-conditions.\<close> |
76 |
76 |
77 end |
77 end |