Proving the correctness of a binary search procedure with SPARK/Ada 
Introduction   SPARK/Ada is a language derived from Ada that allows for a formal checking (i...
Tags: spark, ada, formalchecking, tutorial