Note: Please attend class and the labs for more description.

You must develop (in Rodin) a defensive version of the binary search:

        CONTEXT
		BSD_C0 	›Binary Search (Defensive)
	CONSTANTS
		f	 ›the abstract array
		x	 ›element to look for in the array
		N	 ›
	AXIOMS
		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 -∞
		axm4:	x < f(N) not theorem ›f(N) is ∞
	END

We are looking for element x in function f, but it may not be in the range of the function. The initial model is as follows:

MACHINE
		BSD_M0 	›Specification: we find two consecutive elements of f (f(r) and f(r+1))
		         such that f(r) ≤ x < f(r+1). We have not yet asserted that r is an index, e.g.
		         -∞ 1 4 3 5 ∞
		         -1  0 1 2 3 4 
		        
		        x = 3
		        N = 4
		        r = 0
	SEES
		 BSD_C0 
	VARIABLES
		r	 ›index so that f(r)=x if it is in the array
	INVARIANTS
		inv1:	−1 ≤ r ∧ r < N not theorem ›
	EVENTS
		INITIALISATION:	 not extended ordinary ›
			THEN
				act1:	r :∣ −1 ≤ r' ∧ r' < N ›
			END

		find:	 not extended ordinary ›
			ANY
				i	 ›
			WHERE
				grd1:	−1 ≤ i ∧ i < N not theorem ›
				grd2:	f(i) ≤ x ∧ x < f(i+1) not theorem ›
			THEN
				act1:	r ≔ i ›
			END

	END

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:

b ≔ bool((∃ i · 0 ≤ i ∧ i < N ∧ f(i) = 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.

TBA