Archive
Contracts arrive in C++26 !
In June 2025 the ISO C++ standards committee voted to include function contracts in C++26. At the time of writing this, the latest draft specification is N5014 which includes the syntax and semantics of the support for contracts.
This post will compare the C++26 syntax with the syntax used by Escher C/C++ Verifier (eCv), examine how easily we can extend eCv to handle the C++26 syntax, and compare the strengths and weaknesses of the C++26 support for contracts with eCv from the perspective of compile-time verification.
Read more…Verifying the Liskov Substitution Principle in C++ code: Part 1
When RTCA released DO-178C – the long-awaited update to the DO-178B standard for airborne software – they added a number of supplements to cover specific software development techniques. One of those techniques is object-oriented software development, covered by supplement DO-332. This supplement mentions the Liskov Substitution principle (hereafter abbreviated LSP) in FAQ #14 “Why is the Liskov Substitution Principle (LSP) important?” and gives more detail in FAQ #15 and #16. So, what is the LSP, and how can we make sure that a software design adheres to it? Read more…
Verifying programs that use ‘sizeof’
Consider the following code snippet (based on a real example of critical embedded software), whose purpose is to serialize some data and send it to another piece of hardware: Read more…
Verifying pointer arithmetic
Today I’ll look at whether code that uses pointer arithmetic is any harder to verify than equivalent code that does not use pointer arithmetic.
Consider this function for copying an array (or part of an array) into another array (or part of another array):
void arrayCopy(const int* src, int* dst, size_t num) {
size_t i;
for (i = 0; i < num; ++i) {
dst[i] = src[i];
}
}
Aliasing and how to control it
Today I’ll start by writing a simple function that determines the maximum and minimum of two integers. We want to return two values, and C doesn’t make that easy unless we declare a struct to hold them. So I’ll pass two pointers to where I want the results stored instead. Here goes:
#include "arc.h" void minMax(int a, int b, out int *min, out int *max) post(*min <= a; *min <= b; *min == a || *min == b) post(*max >= a; *max >= b; *max == a || *max == b) { *min = a < b ? a : b; *max = a > b ? a : b; }
I’ve highlighted the ArC annotations in green. Read more…
Verifying absence of integer overflow
One class of errors we need to guard against when writing critical software is arithmetic overflow. Before I go into detail, I invite you to consider the following program and decide what it prints:
#include <stdio.h>
int main(int argc, char *argv[]) {
unsigned int x = 42;
long y = -10;
printf("%s\n", (x > y ? "Hello, normal world!" : "Hello, strange world!"));
return 0;
}
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(const int16_t * array readings, size_t numReadings) pre(readings.lwb == 0; readings.lim == numReadings) pre(numReadings != 0) post(result == ? /* sum of elements of readings */ /numReadings) { int sum = 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:
forall ind in arr.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(const LinEntry* array table, size_t nElems, uint16_t key) post(result <= nElems);
Need help with using C or C++ in critical systems? Click on my picture above.
David Crocker's Verification Blog 