Search Specs

Searching Search spec

We begin with a spec for a procedure to search an array for a given element. Again, this is an APROC rather than a FUNC because there can be several allowable results for the same inputs. APROC Search(q, t) - Int RAISES {NotFound} = <><= i="i" \="\"> RET i [*] RAISE NotFound FI Or, equivalently but slightly more concisely, and highlighting the changes with boxes: APROC Search(q, t) - Int RAISES {NotFound} = <> RET i [*] RAISE NotFound FI Sequential search code Here is code for the Search spec given above. It uses sequential search, starting at the first element of the input sequence. APROC SeqSearch(q, t) - Int RAISES {NotFound} = <> IF q(i) = t = RET i [*] i + := 1 FI OD; RAISE NotFound Alternative search spec Some searching algorithms, for example, binary search, assume that the input argument sequence is sorted. Such algorithms require a different spec, one that expresses this requirement. APROC Search1(q, t) - Int RAISES {NotFound} = <> HAVOC [*] VAR i :IN q.dom | q(i) = t = RET i [*] RAISE NotFound FI Alternatively, the requirement could go in the type of the q argument: APROC Search1(q: Q SUCHTHAT Sorted(this), t) - Int RAISES {NotFound} = <><...> This is farther from code, since proving that a sequence is sorted is likely to be too hard for the code’s compiler. You might consider writing the spec to raise an exception when the array is not sorted: APROC Search2(q, t) - Int RAISES {NotFound, NotSorted} = <> RAISE NotSorted ... This is not a good idea. The whole point of binary search is to obtain O(log n) time performance (for a sorted input sequence). But any code for the Search2 spec requires an O(n) check, even for a sorted input sequence, in order to verify that the input sequence is in fact sorted. This is a simple but instructive example of the difference between defensive programming and efficiency. If Search were part of an operating system interface, it would be intolerable to have HAVOC as a possible transition, because the operating system is not supposed to go off the deep </></...></></></></></=></>