Differences

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

--- assignments:a2 [2013/03/15 21:27] – jonathan
+++ assignments:a2 [2013/03/17 20:27] (current) – jonathan
@@ Line 18: / 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 67: / Line 67: @@
 </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.
-  *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.
+  *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