Document Number: P1334R0 Specifying Concrete Semantics Directly in Contract-Checking Statements Joshua Berne - jberne4@Bloomberg.net John Lakos - jlakos@Bloomberg.net Revised Monday, November 26, 2018 ABSTRACT ======== The existing design of contracts, based on a long history with related features, describes a single mapping of abstract 'levels' onto specific semantics, with those semantics choosable at translation time for each level. Support for levels, though proven over the years to be eminently useful in practice, is nonetheless just a convenient abstraction layered ON TOP OF the more primitive and integral capability of specifying the concrete semantic directly in the CCS itself. Having identified five useful and implementable CCS semantics (defined precisely in P1333R0), we now propose to allow one of five additional identifiers with special meaning (referencing those respective semantics) to be embedded directly within a CCS -- i.e., in lieu of a level name (though those too are still supported), thereby obviating resolution of that CCS's associated semantics (e.g., on the command line) at build time. Table Of Contents ================= 1. History 2. Motivation 3. Wording 1. History ---------- The initial design of contracts was borrowed, in part, from a library-based model pioneered at Bloomberg in which there were only two semantic options: (1) Check the predicate at runtime (and, if it evaluates to false, invoke the handler), or (2) elide the contract check completely (i.e., don't even check the syntax). Given this highly limited set of alternative semantics, the notion of a linear progression seemed to make sense -- e.g., 'OFF', 'critical', 'default', 'audit'. In the model described in P0542R5 (adopted in Rapperswil, 2018) for C++20, we dropped 'critical' (intended to be enabled even on optimized/production builds), and added 'axiom' (so expensive or difficult to check that we never even try). Now that contracts have been integrated successfully into the C++ language itself, however, there is no longer just a linear scale, and in fact, for many important use cases (e.g., independent semantics across contract-checking statements (discussed briefly below), it now make sound engineering sense to specify the intended semantics of a contract-checking statement (CCS) directly in the statement itself. 2. Motivation ------------- There are two well-understood, specific use cases motivating the need for specifying contract-checking statement (CCS) semantics directly in a CCS itself (see also P1331R0 and P1332R0) independently of the semantics chosen for any of the available levels: (1) In a given mature production deployment, we may have working CCSs that are set to a trusted semantic such as "assume" or "check (never continue). We may at some point decide to add new precondition checks -- e.g., because there were none there before, or we've decided to narrow the contract that was specified. In either case, we're not sure that those new checks are being followed, and we certainly don't want to "assume" that they are, or even presume that they are (by actively checking at runtime) and bring down the program if they aren't. At the same time, we don't want to affect any checks that we know currently are being followed ubiquitously. Our need is to add new CCSs, but having a different semantic, such as "check (maybe return)" or perhaps even "check (always return)" -- each enabling distinct optimization (code-eliding) characteristics for the compiler. In this way, we can continue to run with mature checks set to the more-trusting semantic, while we use a less-trusting one for the purposes of diagnosing would-be out-of-contract calls. (2) If we are using conventional translation units (TUs) -- i.e., not modules -- there is currently no way to ensure that the respective contract-level semantics used to build the library will be the same as those used to build the client. By allowing the concrete CCS semantic to be specified directly in the CCS itself, we necessarily preserve that unique semantic across TUs -- irrespective of any contract build modes. (Note that we could then leverage this mechanism within modules to "bind" each of the three named contract-checking levels ('default', 'audit', and 'axiom') to an appropriate contract-checking semantic for export if and as desired.) Finally, by ensuring each distinct CCS semantic is (a) fully defined, and (b) referenceable by its corresponding special identifier, we unleash great potential for exploring other abstractions built on these intrinsic, inherently needed, primitive capabilities. What's more, should the day ever come when a valid and useful ("canonical") sixth CCS semantic is discovered, the additional wording needed to incorporate it into the C++ standard will be the absolute minimum conceivable! 3. Wording ---------- This section is written as if the names chosen for the five CCS semantics are respectively (1) "assume", (2) "ignore", (3) "check_never_continue", (4) "check_maybe_continue", and (5) "check_always_continue" -- acknowledging fully that other names -- such (5) "test_yes_return" -- are plausible. This section also assumes that the wording in section 3 of P1333R0 has been adopted. 5.10 Table 4 - Add the five semantic names to the list of "identifiers with special meaning". 9.11.4.1.1 Syntax Grammar For all of contract checking statement, contract-level becomes contract-mode, defined in this section as: contract-mode: contract-level | contract-semantic contract-semantic: assume | ignore | check_never_continue | check_maybe_continue | check_always_continue 9.11.4.3.1 Checking contracts Change 'If the contract-level of a contract-attribute-specifier is absent' to 'If the contract-mode of a contract-attribute-specifier is absent'. 9.11.4.3.3.b - add The semantic for all contracts in a translation unit with a particular contract-level will be the chosen semantic for that level. 9.11.4.3.3.b-2 - add in A contract with a 'contract-semantic' specified will have the semantic that corresponds to that special identifier ('assume', 'ignore', 'check_never_continue', 'check_maybe_continue', or 'check_always_continue')