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

# File : binary_search.ads

packageBinary_SearchwithSPARK_ModeistypeOpt_IndexisnewNatural;subtypeIndexisOpt_Indexrange1 .. Opt_Index'Last - 1; No_Index :constantOpt_Index := 0;typeArrisarray(Indexrange<>)ofInteger;functionSorted(A : Arr)returnBooleanis(forallIinA'Range=> (forallJinI .. A'Last => A (I) <= A (J)));functionSearch(A : Arr; V : Integer)returnOpt_IndexwithPre => Sorted(A), Post => (ifSearch'ResultinA'RangethenA(Search'Result) = Velse(forallIinA'Range=> A(I) /= V));endBinary_Search;

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

# File : binary_search.adb

packagebodyBinary_SearchwithSPARK_ModeisfunctionSearch(A: Arr; V: Integer)returnOpt_IndexisL,R,M : Opt_Index;beginif(A'First > A'Last)thenreturnNo_Index;endif; - L := A'First; R := A'Last;whileL <= RlooppragmaLoop_Invariant (A'First <= L);pragmaLoop_Invariant (R <= A'Last);pragmaLoop_Invariant (forallIinA'First .. L - 1 => A(I) < V);pragmaLoop_Invariant (forallIinR + 1 .. A'Last => V < A(I)); M := L + (R - L) / 2;ifA(M) < VthenL := M + 1;elsifA(M) > VthenR := M - 1;elsereturnM;endif;endloop;returnNo_Index;endSearch;endBinary_Search;

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

# File : test_search.adb

withBinary_Search;useBinary_Search;withAda.Text_IO;useAda.Text_IO;procedureTest_SearchisA :constantArr := (0, 0, 1, 1, 3, 4, 5, 8, 8, 10, 12, 15, 17);procedureTest(V:Integer)isR : Opt_Index;beginR := Search(A,V);ifR /= 0thenPut_Line ("Found value" & Integer'Image(V) & " at index" & Opt_Index'Image(R));elsePut_Line ("Value" & Integer'Image(V) & " not found");endif;endTest;beginTest(1); Test(6);endTest_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 |