Simple Contracts for C++

We present a minimal system for expressing interface requirements as contracts. They provide basic mitigation measures for early containment of undesired program behavior. The set of facilities suggested in this proposal is deliberately kept to the minimum of preconditions and post-conditions. Contracts are part of an operation’s interface, but not part of its type. That is, while the expression of contracts is logically part of the operation’s interface, the actual code verifying the conditions are part of the operation’s implementation. 1 WHAT ARE CONTRACTS? Contracts are requirements that an operation puts on its arguments for successful completion and set of guarantees it provides upon successful completion. The former is known as pre-condition and the latter is called post-condition. Contracts are part of the interface of an operation as a programmer (consumer or producer) sees it, e.g. “What do I have to do to call this function?” and “What may I rely on when implementing this function?” However, contracts (as suggested in this proposal) are not part of the type system. Contracts are not a general error reporting mechanism, nor are they substitute for testing frameworks. Rather, they offer a basic mitigation measure when a program goes wrong because of mismatch of expectations between parts of a program. Contracts are conceptually more like structured assert() integrated into the language, playing by the language semantics rules – therefore basis for principled program analysis and tooling. There is a strong desire in the C++ community, as evidenced by the number of contracts proposals [1] [2] [3] [4] [5] [6] and continued discussions in the C++ committee (e.g. at the Urbana, IL, 2014 meeting) for language support to express contracts directly in a program. 1.1 CONTRACTS: INTERFACE SPECIFICATION Contracts are part of the interface of an operation, but not part of its type. A contract expresses what the caller of a function must do to satisfy the expectations the callee places on its arguments. Consequently, the expression of a contract must logically be part of the declaration of the operation. N4415 Simple Contracts for C++ 2 1.2 CONTRACTS: CHECKING IS IMPLEMENTATION For simplicity and usability reasons, contracts are not part of the type of an operation. However, ideally, a function invocation should display the same observable behavior whether the function is called directly (e.g. by name) or indirectly (e.g. via a pointer to function). Therefore, the checking of contract, the concrete codes asserting the requirements or the promise an operation makes, must conceptually be part of the implementation of the operation. 1.3 SYNTAX So, how we do express contracts in code? Clearly we need a syntactic place to put a pre-condition or a post-condition. There are various ways to achieve this. Either a contract is expressed in the declaration of a function, or it is expressed separately through a “proclamation” declaration of some sort. The one concern with expressing contracts in declaration is that the “obvious” place to put contracts is becoming “crowded”. An advantage of specifying a contract in a proclamation declaration is that it could be done “retroactively, after the fact” separate from function declaration and does not need to compete for the syntactically crowded space. However, this is also a problem as one must now maintain coherence between declarations, definitions, and proclamations. Furthermore, member functions can be declared only once and a general design principle of C++ is that all that is to be known about a class “interface” is known at the closing brace of its definition. Therefore, contracts must appear in the function declaration – not as a post facto extension. Should we reach out for new keywords, e.g. expects for pre-conditions and ensures for post-conditions? This proposal takes an alternative route and suggests the use of C++ attributes for expressing contracts:  [[expects: condition]] for saying that an operation expects condition to hold for a call to complete successfully  [[ensures: condition]] for saying that an operation guarantees condition to hold after a successful call For example, a pre-condition contract of the indexing operator of a Vector class could be written: T& operator[](size_t i) [[expects: i < size()]]; Similarly, a post-condition contract on a constructor of an ArrayView class could be expressed as: ArrayView(const vector& v) [[ensures: data() == v.data()]]; Note that in a correct program, contracts can be freely ignored without changing the observable behavior. This is in line with the general understanding of semantics impacts of attributes on correct programs. 1.4 OPERATIONAL SEMANTICS The simplest operational semantics of a contract is as follows:  The “condition” of a contract (pre-condition or post-condition) is type-checked in the scope of the function’s parameter declarations. For a member function, that includes the enclosing class’s scope. The same holds for any (friend) function lexically declared in a class. N4415 Simple Contracts for C++ 3  The pre-condition of an operation is evaluated before any other statement in the function’s body. If the result is true, then normal control of execution continues to the first statement in the body of the function. Otherwise, further execution is not guaranteed: either the program aborts, or throws an exception, or if it is allowed to continue then the behavior is undefined. Whichever of these alternatives is chosen is implementation-defined. That is, an implementation may offer translation modes to check all contracts, or only pre-conditions, or only post-conditions, or ignore contract checking.  Similarly, the post-condition is evaluated after evaluation of the return value (if any) and after the destruction of any local variables, but before control is transferred back to the caller. If the evaluation yields true then control continues as it normally would. Otherwise, the program is abnormally terminated as in the pre-condition case. Note that the post-condition of a function is not evaluated as part of an exceptional transfer of control. 1.5 CONTROL OF CONTRACT ASSERTIONS As explained in the previous section, the basic conceptual model of pre-condition or a post-condition is as if the expression assert(condition) is evaluated at the appropriate place. There are several design choices and practical considerations here. First, there ought to be an ability to turn on and off contract checking, or just to enable partial contract checking (e.g. only pre-conditions, or only post-conditions). We do not believe that this facility has to be in form of “feature test macros” accessible in the source program. Remember that for a correct program executed with correct data, ignoring contracts (e.g. turning contract checking off) should not have any effect on permissible observable behavior of the program. It is in some sense a form of optimization – dead code removal. Consequently, we encourage implementations to offer switches to select level of contract checking: on, off, pre-condition only, post-condition only. Second is the question of the granularity of control. Should contract checking be control per function declaration basis, per class definition, per namespaces, per translation, or just whole sale program? Clearly, a per-function or whole-program control is impractical for most programs. Similarly, a per-class or per-namespace control is a road to anarchy. This proposal suggests a per-translation unit control of contract assertion. Finally, an std::abort() in case of contract failure may not be appropriate for some programs – despite the fact that today, a contract failure results in undefined behavior; at least as far as standard library components are concerned. For programs that can afford it or need it, it might makes sense for implementations to offer throwing exceptions (such as std::precondition_failure, std::postcondition_failure) instead of an unrecoverable program termination via std:abort(). However, it is a critical design criteria that contracts be usable in embedded systems or other resourceconstrained systems that cannot afford exceptions. A callback mechanism with setting of various pointers to functions to control contract assertion is equally challenging in terms of removing “dead codes” – many safety-critical systems operate under strict policies of not including codes they don’t run. Consistent with EWG’s expressed preference at the 2014 Urbana, IL, meeting, we recommend that the means of contract assertions be implementation-defined, but should allow “all, none, pre-condition, postcondition” contract checking on per translation unit basis. N4415 Simple Contracts for C++ 4 1.6 FACILITIES DELIBERATELY LEFT OUT This proposal has an extreme focus on simplicity and deliberately leaves out several facilities found useful in more elaborate “programming by contracts” systems. These include “invariants”, “abstract states”, ability to reference “old” values of a parameter upon entry in function-body, reference to the return value of a function in a post-condition, conditions on exceptional transfer of control, etc. These facilities are left out not as a result of value judgment about their usefulness. Rather, we put a premium on simplicity and an evolutionary approach to contracts for C++. Note that there are at least two notions of invariants: (1) representation invariants; and (2) logical invariants. A representation invariant is generally about the object representation of a class, whereas a logical invariant expresses invariants about the abstract data structure that a class is designed to materialize. For example, take a RedBlackTree class designed to represent a red black tree. Assume further that a RedBlackTree object contains the root node as member. A representation invariant expresses a constraint on that root node (i.e. the direct member of the tree object) that it is colored “b