Differences

This shows you the differences between two versions of the page.

--- assignments:a2 [2013/03/15 21:02] – jonathan
+++ assignments:a2 [2013/03/17 20:27] (current) – jonathan
@@ Line 4: / Line 4: @@
 ===== Question 1: Defensive Binary Search  =====
-You must develop (in Rodin) a defensive version of the binary search
+**Note**: Please attend class and the labs for more description.
+You must develop (in Rodin) a defensive version of the binary search:
 <code>
@@ Line 16: / Line 18: @@
 		axm1:	0 ≤ N not theorem ›
 		axm2:	f ∈ −1 ‥ N → ℤ not theorem ›the actual array is f ∈ 1 ‥ N-1 → ℤ
-		axm3:	f(−1) < x not theorem ›f(-1) is -∞
+		axm3:	f(−1) < x not theorem ›f(-1) is -∞, i.e. the index before the array
-		axm4:	x < f(N) not theorem ›f(N) is ∞
+		axm4:	x < f(N) not theorem ›f(N) is ∞, i.e. the index after the array
 	END
 </code>
@@ Line 58: / Line 60: @@
 </code>
-In the initial model, we do not (yet) introduce the precondition that the array is sorted. Thus ''grd2'' finds a potential (but not yet actual) candidate for the index r so that f(r)=x. The comment shows an (unsorted) array for which the model returns index 0 (i.e. f(0)=1) which is not correct. However, together with a later assumption that the array is sorted, ''grd2'' does yield the appropriate binary sort specification. You must now refine the initial model down to final code. The following refinement strategy might be productive:
+In the initial model, we do not (yet) introduce the precondition that the array is sorted. Thus ''grd2'' finds a potential (but not yet actual) candidate for the index r so that f[r]=x. The comment shows an (unsorted) array for which the model returns index 0 (i.e. f(0)=1) which is not correct. However, together with a later assumption that the array is sorted, ''grd2'' does yield the appropriate binary sort specification. You must now refine the initial model down to final code. The following refinement strategy might be productive:
   * In refinement BSD_M1, introduce variables m and n so that the slice m..n is initially -1..N. Two new convergent events look_left and look_right can be used to reduce the slice in which x potentially resides.
   * In refinement BDS_M2, introduce a "found" boolean variable b so that event ''find'' can be refined with the action:
@@ Line 64: / Line 66: @@
 b ≔ bool((∃ i · 0 ≤ i ∧ i < N ∧ f(i) = x))
 </code>
-  * For refinement BDS_M3, you will want a new context that sees the initial context and asserts that f is sorted. You should be able to prove that the following guard of ''find'' (in this refinement) is a **theorem**: (∃ i · 0 ≤ i ∧ i < N ∧ f(i) = x) ⇔ f(m) = x. The specification for defensive "search" part of binary search is now complete, i.e. b is true precisely when x is in the array, and r is an index so that f(r)=x.
+  * For refinement BDS_M3, you will want a new context that sees the initial context and asserts that f is sorted. You should be able to prove that the following guard of ''find'' (in this refinement) is a **theorem**: (∃ i · 0 ≤ i ∧ i < N ∧ f(i) = x) ⇔ f(m) = x. The specification for defensive "search" part of binary search is now complete, i.e. b is true precisely when x is in the array, and r is an index so that f[r]=x.
+  *In the last refinement BSD_M4, you can refine the look left events to use the midpoint (n ≔ (m+n) ÷ 2) and likewise with the look right (m ≔ (m+n) ÷ 2) to obtain the required efficiency.
+  * Finally, you must use the merging rules to obtain the sequential code.
+  * You must discharge all the relevant proof obligations.
+Submit your development electronically. As well, use Latex to produce a report of each part of the model as well as the final code. Justify the final code via the merging rules.
+Note: You might want to compare this development with the development described by Abrial in the text.
+====== Question 2 ======
+TBA