changeset 111:442a87dc1f76

A proof that an imperative binary search is doing the same as the one we proved correct
author Sigurd Meldgaard <stm@daimi.au.dk>
date Tue, 11 Aug 2009 11:24:23 +0200
parents fb3e0d320df6
children d4c60fc2ac0a
files hoare_binsearch.thy
diffstat 1 files changed, 56 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hoare_binsearch.thy	Tue Aug 11 11:24:23 2009 +0200
@@ -0,0 +1,56 @@
+theory hoare_binsearch
+imports "proof_binary" Vcg
+begin
+
+hoarestate vars =
+ U :: nat
+ L :: nat
+ M :: nat
+ bids :: "nat \<Rightarrow> int"
+
+procedures
+ Binsearch (bids ::"nat \<Rightarrow> int", L::nat, U::nat| U ::nat)
+ where M::nat in
+  "WHILE (\<acute>L < \<acute>U)
+  INV {| True |}
+  VAR MEASURE \<acute>U - \<acute>L
+  DO
+      \<acute>M:==(\<acute>L+\<acute>U) div 2;;
+      IF \<acute>bids \<acute>M \<le> 0 THEN
+          \<acute>L:==\<acute>M+1
+      ELSE
+          \<acute>U:==\<acute>M
+      FI
+  OD"
+
+lemma (in Binsearch_impl) Binsearch_spec:
+  shows "\<Gamma>\<turnstile>\<^sub>t {|\<acute>L=l \<and> \<acute>bids=f \<and> \<acute>U = u \<and> l < u |}
+  \<acute>U :== PROC Binsearch(\<acute>bids, \<acute>L, \<acute>U)
+  {|\<acute>U = (binsearch \<acute>bids 0 l u)|}"
+  apply (hoare_rule HoareTotal.ProcRec1)
+  apply (hoare_rule anno=
+    "WHILE (\<acute>L < \<acute>U)
+    INV {| binsearch \<acute>bids 0 l  u = binsearch \<acute>bids 0 \<acute>L \<acute> U|}
+    VAR MEASURE \<acute>U - \<acute>L
+    DO
+    \<acute>M:==(\<acute>L+\<acute>U) div 2;;
+    IF \<acute>bids \<acute>M \<le> 0 THEN
+          \<acute>L:==\<acute>M+1
+      ELSE
+          \<acute>U:==\<acute>M
+      FI
+  OD"
+    in HoareTotal.annotateI)
+proof (vcg, auto)
+  fix L U bids
+  show "\<lbrakk>L < U; bids ((L + U) div 2) \<le> 0\<rbrakk>
+       \<Longrightarrow> binsearch bids 0 L U = binsearch bids 0 (Suc ((L + U) div 2)) U"
+    using binsearch.simps[of bids 0 L U] mid_def by auto
+  show "\<lbrakk>L < U; \<not> bids ((L + U) div 2) \<le> 0\<rbrakk>
+       \<Longrightarrow> binsearch bids 0 L U = binsearch bids 0 L ((L + U) div 2)"
+    using binsearch.simps[of bids 0 L U] mid_def by auto
+  show "\<lbrakk>\<not> L < U\<rbrakk> \<Longrightarrow> U = binsearch bids 0 L U"
+    using binsearch.simps[of bids 0 L U] by auto
+qed
+
+end 
\ No newline at end of file