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 of the program: 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 tha