Contract Support: Defining the Minimum Viable Feature Set

We observe that "C++20 contracts" consisted of two parts. One part was clear, well understood, widely agreed upon, and useful to various groups of C++ users. The other part rose a lot of controversies for various reasons and ultimately led to the removal of the entire feature.

In paper [P2114r0] we have listed a subset of use cases we believe represent useful improvements to the language, offer an incalculable positive value for most users, and reflect the uncontroversial part of "C++20 contracts". In this paper we provide the rationale for our choice. We wish to show that our selection:

• is big enough to be called a Minimum Viable Product (MVP) and get support of the majority of C++ programmers;
• is small enough that we can make it ready in a relatively short period of time;
• does not require controversial design, or features not already implemented in other languages;
• does not prevent the addition of any of the remaining features of "C++20 contracts", or other discussed alternatives, in subsequent stages.

T& Container::get(int i)
  [[pre: i >= 0]]       // precondition
  [[pre: i < size()]]   // precondition
{
  [[assert: buffer_ != nullptr]];  // block-scope invariant
  return buffer_[i];
}

T& Container::get(int i)
{
  if ((i >= 0) == false) { std::cerr << violation("i >= 0"); std::abort(); }
  if ((i < size()) == false) { std::cerr << violation("i < size()"); std::abort(); }
  if ((buffer_ != nullptr) == false) { std::cerr << violation("buffer_ != nullptr"); std::abort(); }
  return buffer_[i];
}

2. Analysis

In this document we use the term C++20 Contracts to refer to contract support facilities in C++ Standard draft just before the removal — [N4820] (which is effectively equivalent to [P0542R5]) — as well as pieces of the associated proposals seen by EWG that had support in polling, such as:

• [P1290R3]
• [P1344R1]
• [P1429R3]
• [P1607R1]
• [P1711R0]

[P2076r0] lists the points of disagreement about the previous incarnation of contracts design:

• Continuation Mode
• Build Levels
• Global Toggles (also known as: external remapping controls)
• Literal Semantics (also known as: in-source controls)
• Assumptions

We observe that all these features fall into category "controlling the tools" in our model. We claim that if we eliminated the use cases for fine-grained tool control, the remainder would still satisfy a huge, consistent and well understood demand. Addressing it would be a valuable and usable feature that would offer a great help in enforcing program correctness. The value in preventing bugs and enforcing program correctness comes from being able to:

1. Just express preconditions, postconditions, and assertions as C++ predicates. This enables a portable language for communicating what constitutes a bug. This information can be consumed by many different tools as well as human programmers.
2. Transform them into runtime-checks at an all-or-none granularity, leaving open the design of finer control to future work. This enables the guarantee that program will never continue after detecting a bug defined by the contract annotations.

In the reminder of the paper we elaborate on the features of MVP and show how they are motivated by the use cases nominated in [P2114r0]. We also discuss how the support for the remaining use cases can be added atop of MVP in subsequent phases.

2.1. Features in MVP

We selected the minimal use cases to allow the widest benefit for the most general section of users, without resorting to known points of contention. We had in mind a simple feature that consisted of the C++20 Contract syntax, a single build option to enable or disable checks, and a (conditionally) user-definable violation handler that is invoked when runtime-enabled checks are violated.

2.1.1. Contract declarations

The most important thing is the ability to express the predicates in function declarations as compiler-checked C++ expressions. This is uncontroversial. This enables:

• compiler to report type-system errors from incorrectly spelled constraints
• generation of run-time code — such as contract checks, or unit tests
• annotation aware static analysis

The contract annotations look like this:

int Accumlator::running_max(int i)
  [[pre: i >= 0]]     // precondition
  [[post r: r >= 0]]  // postcondition
{
  [[assert: stored_ >= 0]];  // block-scope invariant
  return stored_ = std::max(i, stored_);
}	

Compared to C++20 contracts, there is no room for contract-levels: default, audit or axiom. Also no room for "literal semantics", such as ignore. We only have a predicate and, in the case of postconditions, the name of return value.

In fact, this feature alone would already satisfy many users.

Use cases covered:

• dev.reason.knowl
• dev.readable.syntax
• dev.readable.keywords
• dev.parsable
• dev.tooling
• cppdev.syntax.familiar
• cppdev.syntax.cpp
• cppdev.syntax.reuse
• cppdev.location
• api.communicate.inputsoutputs
• api.establish.preconditions
• api.establish.postconditions
• api.express.values
• api.contract.errorhandling
• arch.nomacros
• arch.complete
• sdev.bestpractices
• jdev.understand.contracts
• jdev.understand.keywords
• adev.fast
• teach.bestpractices
• teach.standardized
• teach.portable

2.1.2. Turning on and off all runtime checks

We believe it is essential that we meet two somewhat contradictory requirements:

1. A guarantee that some action is taken whenever a contract is violated
2. A guarantee that there is no runtime overhead for encoded contracts

The former is a correctness requirement, and the latter is performance requirement (after assurance — further discussion about assurance can be found in [P1517R0]).

This suggests that there needs to be at least some control, at build time, over what effect contract annotations have on the final executable. For the MVP we suggest a single flag which turns checking "on" or "off", where:

• "Off" requires that predicates in contract annotations are suntax-checked but otherwise do not affect the resulting executable.
• "On" requires that runtime checks are inserted in place of contract annotations. When any such predicate check returns false, violation handler is invoked.

This is a subset of what [P0542R5] offered, and should come with similar caveats that that proposal had for build modes — where mixing modes is only conditionally supported.

Finer-grained control and additional semantics to failed checks would be left to extensions and future proposals.

Use cases covered:

• dev.reason.sideeffects
• int.conform.postconditions
• int.control.build
• int.runtime.unchecked
• qdev.checkall

2.1.3. Reporting contract violation

On platforms where it makes sense, each contract violation detected at run-time should be reported to the users — including what failed and where in the source code.

Use cases covered:

• api.establish.check
• api.establish.values
• int.conform.violation
• int.violations.information
• jdev.understand.violations
• jdev.understand.aborting
• jdev.understand.buildviolation

2.1.4. Customizing how contract violationa are reported

The semantics and implementation of contract violation handling has significant impact on the extensibility and usability of the feature. However, we cannot offer a fully usable solution without some additional annotations put in individual contract annotations, and this is not proposed for the MVP. What we propose instead is that the Standard only requires that a violation handler is called, but:

• We do not require that the user must be able to customize the handler.
• We do not require that the handler actually logs anything anywhere.
• We do not require a uniform behavior for different contract annotations.
• We do not require that std::abort() or std::terminate() is called at the end of the handler.

However, an implementation that would offer all the above would be conforming.

Use cases covered (implementation defined):

• int.violations.common

2.2. C++20 Contracts Features not in MVP

This section lists use cases that are essential for a contract programming facility, were present in some form in C++20 Contracts, but we decided to leave them out for the MVP.

2.2.1. Continuation after failed run-time check

The ability to control whether a program is halted after a violation handler is called: whether for all runtime-checked contract annotations, or for a subset of them. This would address sdev.maturity and large.newcompiler.

This ability can be introduced on top of MVP as secondary annotations on individual contract annotations (as described in [P1332R0]), and additionally requiring more build modes.

2.2.2. Controlling run-time checks based on cost

The ability to declare the relative cost of runtime-evaluating the predicate inside the contract annotation against the runtime cost of evaluating the function that the contract annotation appertains to would address use cases:

• crit.more.coverage,
• dev.reason.cost,
• crit.production.checking.

Contract levels, such as default and audit, tried to address this, but the design of this feature had flaws:

• The proposed syntax cannot handle templates where the level may depend on template arguments.
• Two levels (or even three) cannot be enough.
• Levels is not enough to convey essential meta information.
• Syntax is not extensible.
• Syntax is uncomfortable.

This functionality can be introduced on top of MVP as annotations indicating how expensive a contract statement is relative to the body of the function.

2.2.3. Injected Facts (Assumptions)

This was highly controversial. An extended analysis can be found in [P2064r0]. Use cases covered: pdev.footgun and hardware.performance.

The best explored use case for this is when there is a single fact injected into a program that is known to produce a huge performance gain; e.g., that the size of some buffer will always be a multiple of 8. Such injected fact can change the performance characteristics of a program from unacceptably slow to realy fast. In that case the risk of corrupting the program is justified. This use case can be handled by a separate feature, such as [P1774r3]. Alternatively, users can stick to vendor-specific extensions, such as __builtin_assume().

The other use case is when all, or a group, of contract annotations is turned simultaneously into multiple injected facts, without previous knowledge if and to what extent this might improve program performance. Turnig literally all contract annotations into injected facts is possible if a programmer installs a custom violation handler containing __builtin_unreachable().

The remaining use case for turning a selected group of contract annotations into injected facts could in principle be achieved in the future by introducing another second-level annotation in contract annotations.

2.2.4. Indicating inexpressible predicates

This woud cover use cases qdev.tooling.control and api.express.unimplementable. Controversies arose because of mixng inexpressibility with levels, and taking word "axiom" to mean __builtin_assume().

Can be implemented atop of MVP either as meta-information on contract declarations, or by annotating functions as inexpressible as described in [P2176r0].

class TimeOfDay
{
  int minutes_;  // since midnight
  [[assert: minutes_ > 0]];    // class invariant
  [[assert: minutes_ < 1440]]; // class invariant
	
pubic:
  explicit TimeOfDay(int mins) 
    [[pre: mins >= 0]]
    [[pre: mins < 1440]];
		
  int minutes() const
    [[post r: r >= 0]]
    [[post r: r < 1440]];
};

void container::push_back(T const& v)
  [[post: size() == oldof(size()) + 1]];
  
void container::push_back(T const& v)
  [[post old_size = size(): size() == old_size + 1]];

3. Conclusion

While the proposed MVP is conservative, we believe that even the MVP may contain a number of unresolved small issues that will require time to polish. With EWG attention almost entirely consumed by controversial bits of C++20 contracts, the uncontroversial bits may not have been given sufficient consideration for attention. If we are to ship any contract programming support in C++23 time frame, we have to be sure that we have a small enough scope to be accommodated by the WG21 process.

The biggest advantage of this MVP is that we provide a standard notation for expressing preconditions and postconditions. This notation will be consumed by many tools, which are not necessarily compilers. The positive effect on the community is not necessarily in what compilers can do with it, but also what other automated tools can get from it. This is far beyond the scope of the C++ Standard.

4. References

• [P2114r0] — Joshua Berne, Ryan McDougall, Andrzej Krzemieński, "Minimal Contract Use Cases"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2114r0.html).
• [P1995r0] — Joshua Berne, Timur Doumler, Andrzej Krzemieński, Ryan McDougall, Herb Sutter, "Contracts — Use Cases"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1995r0.html).
• [P2185r0] — Caleb Sunstrum, "Contracts Use Case Categorization"
  (https://isocpp.org/files/papers/P2185R0.html).
• [N4820] — Richard smith, "Working Draft, Standard for Programming Language C++",
  http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/n4820.pdf).
• [P0542r5] — G. Dos Reis, J. D. Garcia, J. Lakos, A. Meredith, N. Myers, B. Stroustrup, "Support for contract based programming in C++"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0542r5.html).
• [p2076r0] — Ville Voutilainen, "Previous disagreements on Contracts"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2076r0.html).
• [P1774r3] — Timur Doumler, "Portable assumptions"
  http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p1774r3.pdf).
• [P1332r0] — Joshua Berne, Nathan Burgers, Hyman Rosen, John Lakos, "Contract Checking in C++: A (long-term) Road Map"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1332r0.txt).
• [P1517r0] — Ryan McDougall, "Contract Requirements for Iterative High-Assurance Systems"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1517r0.html).
• [P2176r0] — Andrzej Krzemieński, "A different take on inexpressible conditions"
  (https://isocpp.org/files/papers/P2176R0.html).
• [P2064r0] — Herb Sutter, "Assumptions"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2064r0.pdf).
• [P2038r0] — Andrzej Krzemieński, Ryan McDougall, "Proposed nomenclature for contract-related proposals"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2038r0.html).
• [N4160] — Andrzej Krzemieński, "Value Constraints"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4160.html).
• [P1344r1] — Nathan Myers, "Pre/Post vs. Enspects/Exsures"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1344r1.md).
• [P1711r0] — Bjarne Stroustrup, "What to do about contracts?"
  (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1711r0.pdf).