Wiki Agenda Contact Version française

Toccata

Formally Verified Programs, Certified Tools and Numerical Computations

• Home
• Members
• Software
  • Software
  • Gallery of verified programs
• Projects
• Publications
• Jobs

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é

Topics: Arithmetic Overflow / Array Data Structure / Searching Algorithms

Tools: SPARK 2014

See also: Binary Search, Java version / Binary search in C annotated in ACSL

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.

---

---

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'.

---

---

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.

---

---

with Binary_Search; use Binary_Search;
with Ada.Text_IO;   use Ada.Text_IO;


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
         Put_Line ("Value" & Integer'Image(V) & " not found");
      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

---