In their CppCon'23 talk titled “Better Code: Contracts in C++”, Sean Parent and Dave Abrahams of Adobe advise developers on how to use a methodology known as “Design by Contract” to build better and safer systems. While the talk is targeted towards C++ developers, the methodology is fairly general and can be applied to other imperative languages as well. For me, the talk was really fun to watch, so I would definitelly recommend it to others. That said, I have a couple of remarks about the talk that I want to write down and share.
The Talk
The main part of the talk consists of Sean and Dave arguing about what is more important: code or documentation. Along the way, they introduce concepts such as tower of abstraction, Hoare logic, class invariants, Design by Contract, blame, and exception guarantees, while exploring the power and limitations of contracts implemented as dynamic checks in the C++ language.
Static vs Dynamic Checks
And this is the main thing I want to elaborate on: weaknesses of dynamically checked contracts. As Sean and Dave put it: “you can’t check everything”. Some things are too expensive to be checked in runtime (e.g., the precondition of the binary search algorithm), and to check other (like pointer validity), one would need to instrument code (like sanitizers do). In my opinion, this would be one reason for wanting to move from dynamic checks to static checks.
Capturing Old Values of Parameters
Sometimes (for example, at 12:00 of the video), the postcondition of a function needs to relate the
computed result to old values of the function parameters.
However, a dynamic check would require making an actual copy of the parameter (or of an expression involving it).
This is unfortunate for multiple reasons, performance being the obvious one.
As the presenters later note, such requirement may restrict the usability of generic code to copyable types.
For example, consider the following piece of C++ code (taken from 13:20 of the video),
where we want to say that pop_back preserves the value of all elements of the given container except the last one:
template <typename T, typename U>
requires (copyable<T> && assignable<T> && copyable<U> && assignable<U>)
class zip_vec {
private:
vector<T> _first;
vector<U> _second;
public:
size_t size() const { return _first.size(); }
void pop_back()
post [old = *this] { equal(begin(), end(), begin(old)) }
{
_first.pop_back();
_second.pop_back();
}
//invariant { size(first()) == size(second()) }
};
This is another reason for going with static checks instead.
With static checks performed directly on the template, if done properly,
we would not need to restrict T and U.
To do such static checks, we would need to have some language to describe the desired properties.
Before exploring such a language, we would need to think about related concept: values.
What Is a Value?
A program in an imperative language like C++ (or C) manipulates objects.
An object, when interpreted, can have a value.
Another entities that can have a value when interpreted are expressions.
Values are immutable, abstract entities - like the Boolean false, the natural number 3,
the real number π, and so on.
Values do not live inside the “world” manipulated by programs, but rather in a meta-level world.
The specification of a programming language defines the mapping from objects to values, as well as mapping from expressions to values, and also defines how values propagate through operations. For example, the C++ standard says the following:
The result of the binary + operator is the sum of the operands.
Here, sum is a meta-level concept - a meta-level function on values.
Let us write [[o]] to stand for the value of the object o,
and [[e]] for the value of the expression e.
Then we could rewrite the above sentence from the standard in a mathematical notation, as `∀ e1 e2, [[(binary_operator_+ e1 e2)]] = (sum [[e1]] [[e2]]). Ideally, the whole language specification would be precisely captured in such notation.
The language specification can do this only for types that it defines: it does not try to predict what user-defined types are meant to represent, and what is the effect of user-provided operations on values of user-provided types. But what if we allowed the user to specify these relations in a suitable language?
Towards a Language of Static Contracts
Consider the same zip_vec example, this time with contracts written using such notation.
We could first declare a predicate represents as a binary relation between instances of zip_vec
and lists of pairs of T and U. Then, we would say that the default constructor constructs something
that represents an empty list, and that pop_back, if given something representing a list with a pair at its end,
changes that into something representing the list without that pair at the end.
template <typename T, typename U>
class zip_vec {
public:
//@ declare-predicate represents: zip_vec × (list (pair T U)).
//@post: represents (*this) [].
zip_vec();
//@ ∀ (l : list (product T U)) (t : T) (u : U),
//@pre represents (*this) (l ++ [t,u])
//@post represents (*this) l
void pop_back();
};
Of course, this is only the public interface.
It would be up to the private implementation to define the represents predicate
and to ensure that the operations play nice with it.
This way, we do not need to restrict the types of T and U.
Use a separation logic?
Of course, the specification language should have a well-defined meaning. Ideally, we could use a variant of separation logic (SL), which is well-understood in the formal methods community. I was surprised to see that many problems mentioned in the talk are adressed by features of modern separation logics.
And Everything Else Stays Unchanged
In a contract, there is often the implicit promise that “everything else stays unchanged”. That is the essence of separation logic - to separate the part of the heap that changes from the part of the heap that stays the same. Furthermore, as mentioned at time 23:20 in the video, most functions that mutate an object assume that they have a sole access to that object; that nobody else is observing (or mutating) the object in meanwhile. This is also easily, often implicitly, specified in a SL.
Meaningless objects
As mentioned at 31:50, sometimes we want to weaken the invariant of a class to allow for a state
that is invalid for most operations except assignment and destruction.
The typical situation is std::variant, which has a special method, valueless_by_exception,
for its clients to detect such state.
Sean and Dave explain that having such method (or an associated flag in the class)
is often unnecessary, since typically, such state is a result of throwing an exception
in the middle of a mutating operation and can be observed only in catch blocks.
However, this is a kind of an implicit knowledge, in the sense that we do not have a way to test for such condition programmatically and still we informally know when an object can be valueless. If we wanted to programmatically analyze code for situations where a valueless object is used in a way that is not supported, we would have to resort to ad-hoc heuristics. Or, use another feature of most modern separation logics: ghost state.
Ghost state consists of ghost variables, which are mathematical variables that are not part of a program’s
physical state but only part of its logical state. Such variables can not be read or written by the program during execution, but can be written when specifying contracts and reasoning about them.
For classes that can go valueless, we could specify a ghost flag has_value and make all member functions
except destructor and assignment operator require it set as a part of the precondition,
and make all member function preserve it on normal exit paths.
That way, we could easily write a local analysis as Sean suggests at 33:48, but without relying on
an implicit knowledge being hardcoded in the analyzer.
Other remarks
As mentioned in the talk, a contract can be used to determine which part of a code is to be blamed for contract violations. The situation is more complicated in the presence of higher-order functions. Also, there is a lot of literature on the topic of blame, for example Wadler’s Well-Typed Programs Can’t Be Blamed.
Conclusion
Contracts are a powerful mechanism, and it is only good that dynamic contract checking is slowly making it into mainstream languages such as C++. However, contracts and dynamic contract checking are two different things, as typically one does not want to check the whole contract at runtime. I would like to see a formal language that can precisely express the whole contract, even if it could not be checked dynamically. But perhaps, unlike documentation written in a natural language, it would be checkable statically. Maybe a variant of a separation logic adapted for C++ would make C++ a better language.