## Initial setting

So, I was checking a small demo of the WP plug-in the other day, just before making a presentation of Frama-C to some future fellow user. This was the traditional binary_search verification presented in the Berlin training session in 2010, but using the WP plugin instead of Jessie. For some reason, I decided to change the type for all the offsets from `int`

to `unsigned int`

. After all, we're morally dealing with array indexes and we want to search very big arrays (with `length > INT_MAX`

, don't we?), what can possibly go wrong?

The code and its contract then become the following:

/*@ requires length > 0; requires \valid(a+(0..length - 1)); requires sorted: \forall integer i,j; 0<=i<=j<length ==> a[i]<=a[j]; behavior find: assumes \exists integer i; 0<=i<length && a[i] == key; ensures 0<= \result < length; ensures a[\result] == key; behavior no_find: assumes \forall integer i; 0<=i<length ==> a[i] != key; ensures \result == -1; */ unsigned int binary_search(int* a, unsigned int length, int key) { unsigned int low, high; low = 0; high=length-1; while (low <= high) { unsigned int med = (high-low)/2U+low; if (a[med] == key) return med; if (a[med] < key) low = med+1; else high = med-1; } return -1; }

## Loop invariants

As all of you know, deductive verification require to write loop invariants to have a slight chance of proving something. An appropriate set of invariants for our case is the following:

`low`

is between`0`

and`high + 1`

(at the loop exit)`high`

is less than`length`

- all cells before
`low`

contain elements smaller than`key`

- all cells after
`high`

contain elements greater than`key`

and for the termination, we have

- the difference between
`high`

and`low`

strictly decreases.

Translated into ACSL, with named loop invariants in order to easily identify them in WP's output and without forgetting the `loop assigns`

(WP is a bit picky about that), this becomes:

/*@ loop invariant low: 0<=low<=high+1; loop invariant high: high < length; loop invariant smaller: \forall integer i; 0<=i<low ==> a[i] < key; loop invariant greater: \forall integer i; high < i < length ==> a[i] > key; loop assigns low, high; loop variant high - low; */

## A wrong specification!

we launch Frama-C with the following command line:

frama-c-gui -wp -wp-split -wp-rte binary_search.c

`-wp`

asks WP to generate proof obligations (POs) and to launch the default prover (Alt-ergo) on them`-wp-split`

splits POs that are conjunctions, leading to smaller (and hopefully easier to prove) formulas to the provers`-wp-rte`

asks RTE to generate all safety assertions before WP is launched. In other words, we will get proof POs for potential run-time errors.

The result is encouraging, but not perfect: `behavior no_find`

is not proved, and if we dig a little bit in the `WP Proof Obligations`

panel, we see that the branch where the PO fails is the one where we return `-1`

, exactly what we specified:

Of course, returning `-1`

is sensible for indicating failure when we have `int`

s, not so with `unsigned`

... In that case, we can return `length`

to indicate that no suitable index has been found

## Subtraction is not harmless

We thus correct the `ensures`

clause and the return `statement`

according to our new error value and relaunch frama-c-gui. This time, almost everything is fine, except from some tiny assertion from RTE, when assigning `med-1`

to `high`

:

assert rte: med-(unsigned int)1 ≥ 0;

As a matter of fact, if we think of it a little further, if the `key`

is less than all elements of the array, `med`

will become `0`

at a certain point, and we'll try to assign `-1`

to `high`

, which is not exactly what we want (and is likely to result in a buffer overflow at the next loop step if `length<UINT_MAX/2`

). We thus modify our `else`

clause that way:

else { if med == 0 break; high = med - 1; }

## Getting a correct program

This time, all POs are discharged, meaning that the program is correct with respect to its specification. I guess this was yet another example that no change in the code, as small as it looks like, can be considered harmless, and that looking at the unproved POs of WP can be an effective way to catch those issues.