C++ seems to finally converge with their contracts proposal, https://wg21.link/p2900. I decided to give it a try and come up with ideas how such a thing would look for C. This is in early stages, not a full proposal yet, and still would need implementation by some of the major compilers.
In particular, the C++ feature is full of sidetracks that I don’t like at all, such as user-defined global handlers and ignorability. But there is a core of ideas, syntax and semantics that I found interesting and that I think should be considered for C. The principal features are
Contract pre- and postconditions add verifiable conditions that are added to function interfaces. They are checked on entry to a function call and provide knowledge that is valuable for the code following a call.
If the condition is an integer constant expression, a pre- or postcondition is similar to an invocation of static_assert . If the condition is false, compilation fails. In the following we will not illustrate this aspect to simplify the discourse.
. If the condition is false, compilation fails. In the following we will not illustrate this aspect to simplify the discourse. They have no implications on ABI.
They can be made composable. If applied rigorously, such conditions can often be deduced from the context. They need not be checked dynamically.
Besides verified correctness, they offer optimization opportunities for the context of a function call and for the called function itself.
To see how all of this works we first need understand two fundamental primitives, assertions and assumptions. Their syntax looks something like
contract_assert(COND, "some explanatory text"); contract_assume(COND, "some explanatory text");
Here, in both cases COND is some condition that is supposed to be fulfilled.
... continue reading