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)

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. 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;
```

This is then the body, with the code of the main procedure 'Search'. binary_search.adb

```package body Binary_Search
with SPARK_Mode
is

function Search(A: Arr; V: Integer) return Opt_Index is
L,R,M : Opt_Index;
begin
if (A'First > A'Last) then return No_Index; end if;
-      L  := A'First; R := A'Last;
while L <= R loop
pragma Loop_Invariant (A'First <= L);
pragma Loop_Invariant (R <= A'Last);
pragma Loop_Invariant
(for all I in A'First .. L - 1 => A(I) < V);
pragma Loop_Invariant
(for all I in R + 1 .. A'Last => V < A(I));
M := L + (R - L) / 2;
if A(M) < V then L := M + 1;
elsif A(M) > V then R := M - 1;
else return M;
end if;
end loop;

return No_Index;
end Search;

end Binary_Search;
```

Finally, here is a simple test. This part produces output, outside the SPARK fragment, so not analyzed by the proof tools. test_search.adb

```with Binary_Search; use Binary_Search;

procedure Test_Search is
A : constant Arr := (0, 0, 1, 1, 3, 4, 5, 8, 8, 10, 12, 15, 17);

procedure Test(V:Integer) is
R : Opt_Index;
begin
R := Search(A,V);
if R /= 0 then
Put_Line ("Found value" & Integer'Image(V) & " at index" & Opt_Index'Image(R));
else
end if;
end Test;

begin
Test(1); Test(6);
end Test_Search;
```

# Why3 Proof Results for Project "binary_search"

## Theory "binary_search.Binary_search__package_def": fully verified in 0.00 s

 Obligations VC for def split_goal_wp

## Theory "binary_search.Binary_search__sorted__subprogram_def": fully verified in 0.02 s

 Obligations CVC4 (1.5) VC for def --- split_goal_wp 1. assertion 0.00 2. assertion 0.02

## Theory "binary_search.Binary_search__search__subprogram_def": fully verified in 0.77 s

 Obligations CVC4 (1.5) VC for def --- split_goal_wp 1. precondition 0.03 2. precondition 0.02 3. loop invariant init 0.03 4. loop invariant init 0.02 5. loop invariant init 0.03 6. loop invariant init 0.02 7. assertion 0.03 8. precondition 0.02 9. assertion 0.04 10. precondition 0.04 11. precondition 0.02 12. precondition 0.03 13. precondition 0.04 14. assertion 0.04 15. precondition 0.03 16. assertion 0.02 17. precondition 0.03 18. loop invariant preservation 0.05 19. loop invariant preservation 0.02 20. loop invariant preservation 0.04 21. loop invariant preservation 0.05 22. assertion 0.03 23. assertion 0.03 24. postcondition 0.06