note description: "Binary search on integer arrays." class BINARY_SEARCH feature -- Basic operations binary_search (a: SIMPLE_ARRAY [INTEGER]; value: INTEGER): INTEGER -- Index of `value' in `a' using binary search. Return 0 if not found. -- https://en.wikipedia.org/wiki/Binary_search_algorithm#Iterative require -- sorted: across 1 |..| (a.sequence.count - 1) as c all a.sequence [c.item] < a.sequence [c.item + 1] end -- a_sorted: across 1 |..| a.sequence.count as i all -- across 1 |..| a.sequence.count as j all -- i.item <= j.item implies a.sequence[i.item] <= a.sequence[j.item] end end sorted: is_sorted (a.sequence) local low, up, middle: INTEGER do from low := 1 up := a.count + 1 middle := a.count invariant -- TASK 1: Add loop invariants to validate array accesses. valid_bounds: low >= 1 and then low <= up and then up <= a.count + 1 -- TASK 5: Add loop invariants to prove postcondition. valid_result: Result = 0 or (1 <= Result and then Result <= a.count) not_found_low: across 1 |..| (low - 1) as c all a.sequence [c.item] < value end not_found_up: across up |..| a.count as c all a.sequence [c.item] > value end found: Result > 0 implies a.sequence[Result] = value until low >= up or Result > 0 loop middle := low + ((up - low) // 2) if a[middle] < value then low := middle + 1 elseif a[middle] > value then up := middle else Result := middle end variant -- TASK 2: Add loop variant to prove termination. + (up - low) end ensure -- TASK 4: Add postconditions to verify client code. found: Result > 0 implies Result <= a.count and then a [Result] = value not_found: Result = 0 implies not a.sequence.has (value) end is_sorted (a: MML_SEQUENCE [INTEGER]): BOOLEAN note status: ghost, functional do Result := across 1 |..| a.count as i all across 1 |..| a.count as j all i.item <= j.item implies a [i.item] <= a [j.item] end end end end