Binary Search, SPARK/Ada version
Binary Search in an sorted array.
The ZIP file below contains all the necessary source file to compile the code using GNAT and redo the proofs using SPARK.
Authors: Claude Marché
Tools: SPARK 2014
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
This is first the Ada interface, with the protoype of the main procedure 'Search', but also the pre- and post-condition, using the regular Ada 2012 syntax.
File : binary_search.ads
package Binary_Search with SPARK_Mode is type Opt_Index is new Natural; subtype Index is Opt_Index range 1 .. Opt_Index'Last - 1; No_Index : constant Opt_Index := 0; type Arr is array(Index range <>) of Integer; function Sorted(A : Arr) return Boolean is (for all I in A'Range => (for all J in I .. A'Last => A (I) <= A (J))); function Search(A : Arr; V : Integer) return Opt_Index with Pre => Sorted(A), Post => (if Search'Result in A'Range then A(Search'Result) = V else (for all I in A'Range => A(I) /= V)); end Binary_Search;