The ProVal team was stopped at the end of August 2012, and reborn into a new team
Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Binary search in C annotated in ACSL
This is a C version of Binary Search, annotated in ACSL.
Authors: Claude Marché / Jean-Christophe Filliâtre
Topics: Arithmetic Overflow / Searching Algorithm / Tricky termination
References: The VerifyThis Benchmarks
Here is the annotated source code
/*@ predicate sorted{L}(long *t, integer a, integer b) = @ \forall integer i,j; a <= i <= j <= b ==> t[i] <= t[j]; @*/ /*@ requires n >= 0 && \valid_range(t,0,n-1); @ ensures -1 <= \result < n; @ behavior success: @ ensures \result >= 0 ==> t[\result] == v; @ behavior failure: @ assumes sorted(t,0,n-1); @ ensures \result == -1 ==> @ \forall integer k; 0 <= k < n ==> t[k] != v; @*/ int binary_search(long t[], int n, long v) { int l = 0, u = n-1; /*@ loop invariant @ 0 <= l && u <= n-1; @ for failure: @ loop invariant @ \forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u; @ loop variant u-l; @*/ while (l <= u ) { int m = (l + u) / 2; //@ assert l <= m <= u; if (t[m] < v) l = m + 1; else if (t[m] > v) u = m - 1; else return m; } return -1; }
The program above is the classical binary search for a given element in an array sorted in increasing order.
This program exposes a long-standing bug, that is the computation of l+u may overflow. When attempting to prove this program with Frama-C/Jessie, the VC corresponding to this overflow cannot be proved.
See also
- http://en.wikipedia.org/wiki/Binary_search_algorithm
- http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html
- Harvey Tuch, Gerwin Klein, and Michael Norrish. 2007. Types, bytes, and separation logic. In Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’07). ACM, New York, NY, USA, pages 97–108. http://doi.acm.org/10.1145/1190216.1190234