David Crocker's Verification Blog

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.

C++26 pre(…) and post(…)

The committee very sensibly chose to use pre and post to introduce function preconditions and postconditions. It’s vital to encourage programmers to write contracts; choosing short and quick-to-type keywords to introduce them is an excellent start. Keywords pre and post are already well-established for this purpose in SPARK Ada, in eCv and elsewhere. In C++26 these are identifiers with special meaning in certain contexts, to avoid clashing with any uses of these identifiers in existing C++ programs.

The requires and ensures keywords used by some other languages that support contracts are more verbose and harder to type. Some may argue that the keyword completion facility offered by modern editors makes this irrelevant. However, there are many programmers (including myself) who cannot touch-type and therefore find keyword completion of limited value, because of the need to glance upwards to the screen to see what keyword the editor proposes.

One difference from eCv is that instead of allowing multiple preconditions separated by semicolon to be placed inside pre(…) the C++26 syntax requires each expression to be enclosed individually in pre(…). This will encourage programmers to put each precondition on a separate line. This is a good thing when the preconditions are lengthy expressions, but a disadvantage when the expressions are short.

Similarly, multiple postconditions must be individually enclosed by post(…). A further difference in postconditions is that there is no predefined name for the result expression corresponding to result or _ecv_result in eCv. Instead an identifier to represent the result is declared in the postcondition, like this:

post(r : r > 1)

We expect to have no difficulty extending eCv to accept the C++26 precondition and postcondition syntax, while at the same time retaining support for the current eCv syntax for the benefit of existing users. We’ll need to accept multiple pre(…) and post(…) clauses, and we’ll need to support the optional result identifier declaration in post(…) clauses.

C++26 contract_assert

C++26 introduces a new keyword contract_assert which is followed by a parenthesized conditional-expression. This is very similar to the way in which eCv uses assert or _ecv_assert. So to have eCv accept the C++26 syntax we just need to make contract_assert equivalent to _ecv_assert.

Anything else?

In terms of syntax for contracts in C++26, that’s it! The stated intention was to implement a Minimum Viable Product (MVP) for contracts in C++26. So it is understandable that there is a lot missing!

Most surprising is that expressions in C++26 contracts may have side-effects on variables, and it is unspecified whether such side effects occur. eCv requires (and enforces) expressions in contracts to have no side-effects. I will be surprised if the major compilers for C++26 don’t provide the option to generate warnings when contract expressions have side-effects, at least in situations where this is easily detected.

Missing features

Whereas eCv attempts only compile-time verification of contracts, the focus of the C++26 support is on run-time checking of contracts. So it is not surprising that features needed to support compile-time verification are lacking. Features that are amenable to attempting compile-time verification but are difficult to implement run-time checking are also missing.

These are some of the features missing from C++ contract support. All are supported by eCv.

• Contracts for virtual functions. These are vital for object-oriented design-by-contract development. The main issue here is to ensure that when a function in a derived class overrides one in an ancestor class, the Liskov Substitution Principle (LSP) is obeyed.
• Contracts for function pointers. Less important than contracts for virtual functions, but still useful. The LSP rules must be obeyed as for virtual functions.
• The old modifier within postconditions, so that they can refer to the initial value (i.e. at function entry) of a variable as well as the final value.
• Declarations of the frame of a function, which limits what a function may modify. It’s possible to imply a minimal frame from the function signature and additional frame information from the function body; but accurate determination of the frame of a complex function automatically is not always possible.
• Ghost functions (i.e. declarations and implementations of functions that are used only in contracts). Declaring a function as ghost tells the compiler that code need not be generated for these functions, unless run-time checking of contracts is being used. Some compiler/linker combinations such as gcc provide the option to remove un-called functions from the final binary file; nevertheless is it useful to tag functions that are only referred to in contracts.
• Ghost members of array and pointer types, so that array limits and object sizes can be specified and reasoned about. While programming for desktop and server systems typically avoids using arrays, it’s very common to use arrays in embedded C++ programming, especially in real-time systems for which dynamic memory allocation must normally be avoided after the initialization phase.
• Other ghost expressions. eCv provides a wide range of ghost expression types, for example quantifiers. Some of these are needed when writing contracts for C programs but are not needed with C++ because the language itself provides the means to express them, at the expense of needing additional #include directives. For example, the eCv forall and exists keywords when used to quantify over STL collections can be replaced by calls to members of those collections with appropriate lambda function parameters; and the eCv minof and maxof keywords can be replaced by calls to static member functions of numeric_limits. Some other types of ghost expression such as disjoint in eCv cannot be replaced by C++ constructs.

Summary

The arrival of contracts in C++ is very welcome despite their limitations in C++26. The use of the short pre and post reserved identifiers to introduce them is especially good news.

C++26 contracts are aimed primarily at run-time checking. Can they be used for formal verification? Certainly it should be possible in many cases to verify whether or not a call to a function with declared preconditions satisfies those preconditions, especially if the verifier assumes that previously-called functions satisfy their postconditions and previously-passed contract_assert statements are satisfied. However, proving that postconditions are satisfied, and proving that contract assertions are true is likely to be impossible in all but the simplest of cases. In particular, if the postcondition or assertion depends on values computed by one or more loops, then unless the loop can be seen to have only a small number of iterations, verification of the postcondition requires a loop invariant to be declared or computed; and computing loop invariants is in general very difficult.