## Specification with Ghost Functions

In my previous post I showed that the C expression sublanguage extended with quantified expressions (**forall **and **exists**) is insufficient to allow some specifications to be expressed. I presented this function (annotated with an incomplete specification) to average an array of data:

int16_t average(constint16_t *arrayreadings, size_t numReadings)pre(readings.lwb == 0; readings.lim == numReadings)pre(numReadings != 0)post(result== ?/* sum of elements of readings *//numReadings) {intsum = 0; size_t i;for(i = 0; i < numReadings; ++i)keep(i <= numReadings)keep(sum == ?/* sum of first i elements of readings */)decrease(numReadings - i) { sum += readings[i]; }return(int16_t)(sum/numReadings); }

## Expressing the Inexpressible

When writing preconditions, postconditions and other specifications for C programs, sometimes we need to write expressions that can’t be expressed in plain C. That’s why formal verification systems based on annotated programming languages almost always augment the expression sublanguage with **forall **and **exists **expressions. In previous posts, I’ve introduced ArC’s implementations of these. For example, the following expression yields **true **if all elements of the array *arr *are between 0 and 100 inclusive:

forallindinarr.indices :- arr[ind] >= 0 && arr[ind] <= 100

Here, *ind *is declared as a bound variable that ranges over the values in the expression that follows the keyword **in**, which in this case is all the indices into *arr*. Read more…

## Verifying a binary search, part 2

In my last entry I showed how to use a correct-by-construction approach to develop a binary search function. We got as far as specifying the function and the loop, but we left the loop body undefined. The function declaration looked like this: Read more…

## Verifying a binary search

In the last post, I covered some different levels of formal verification that you may be interested in, and showed how to add minimum annotation to the linearization example to allow ArC to prove predictable execution. The example provided a prototype for the binary search function it called, to which we added a minimal postcondition, so that it looked like this:

size_t bSearch(constLinEntry*arraytable, size_t nElems, uint16_t key)post(result<= nElems);