GotW #97: Contracts, part 1 – Assertions and postconditions

As WG21 continues work on contracts, I thought I’d join other WG21ers like Andrzej Krzemieński who are writing ‘explainer’ blog posts about various considerations related to contracts, and to draw attention to the existing work and papers like P0542.

Assertions have been a foundational tool for writing understandable computer code since we could write computer code… far older than C’s assert() macro, they go back to at least John von Neumann and Herman Goldstine (1947) and Alan Turing (1949). [1,2] And postconditions are definitely related… but how, exactly?

JG Questions

1. What is an assertion, and what is it used for?

2. If an assertion fails, what does that indicate, and who is responsible for fixing the failure? Refer to the following example assertion code in your answer.

void f() {
int min = /* some computation */;
int max = /* some other computation */;

// still yawn more yawn computation

assert (min <= max); // A

// ...
}

3. Are assertions primarily about checking at compile time, at test time, or at run time? Explain.

4. C++20 supports two main assertion facilities:

assertstatic_assert

For each one, briefly summarize how it works, when it is evaluated, and whether it is possible for the programmer to specify a message to be displayed if the assertion fails.

Guru Questions

5. What is a postcondition, and how is it related to an assertion?

6. Should postconditions be expected to be true if an exception is thrown? Justify your answer with example(s).

7. Should postconditions be able to refer to both the initial (on entry) and final (on exit) value of a parameter, if those could be different? If so, give an example.

Notes

Thanks to Wikipedia for pointing out these references.

[1] H. H. Goldstine and J. von Neumann. “Planning and Coding of problems for an Electronic Computing Instrument” (Report on the Mathematical and Logical Aspects of an Electronic Computing Instrument, Part II, Volume I, p. 12; Institute for Advanced Study, April 1947.)

[2] Alan Turing. “Checking a Large Routine” (Report of a Conference on High Speed Automatic Calculating Machines, pp. 67-9, June 1949).