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®=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_M1, 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_M2, 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