Document number:   P2521R2
Date:   2022-03-15
Audience:   SG21
Reply-to:  
Gašper Ažman <gasper dot azman at gmail dot com>
Joshua Berne <jberne4 at bloomberg dot net>
Bronek Kozicki <brok at spamcop dot net>
Andrzej Krzemieński <akrzemi1 at gmail dot com>
Ryan McDougall <mcdougall dot ryan at gmail dot com>
Caleb Sunstrum <caleb dot sunstrum at gmail dot com>

Contract support — Working Paper

This paper is a yet another proposal to add a minimum contract support framework to C++. It proposes nothing that hasn't already been described in either [P2388R4] or [P2461R1].

The goal in this paper is to structure the proposal in a different way, in order to reflect what SG21 has consensus on and what remains a controversy. We treat the following as open issues:

  1. The choice of syntax.
  2. Side effect elision and duplication.
  3. The treatment of non-reference function parameters referenced in postconditions.

We assume that the reader is already familiar with [P2388R4].

0. Revision history {rev}

0.1. R0 → R1{rev.r01}

  1. We now disallow contract annotations on function re-declarations and overriding function declarations.
  2. Clarified what happens when a contract predicate contains a call to a virtual function.
  3. Included poll results on including postconditions in the MVP.
  4. Explained why we need mixed translation modes to be implementation-defined.
  5. Removed the text which suggested that implementing runtime precondition checks inside function bodies is a necessity.
  6. Described more special cases related to virtual functions: when a base class is a template parameter, and when a function overrides more than one virtual function.
  7. Clarified that we are aiming at freestanding implementations.
  8. No longer defining look-up in contract annotations by analogy with noexcept.
  9. Mixing translation modes is IFNDR.

0.2. R1 → R2{rev.r02}

  1. Described the proposed evaluation order of preconditions and postconditions. See section {pro.ord}.
  2. Non-reference function parameters named in the postcondition must be declared const. See section {pro.arg}.
  3. Explained why reading the value of function arguments instead of function parameters cannot solve the problem of non-reference function parameters referenced in postconditions. See section {pro.arg.out}.
  4. Changed the motivation for adding side effect removal: it is not efficiency, it is the intention to discourage programmers from deliberately putting side effects in contract annotations.

1. Motivation {mot}

The motivation for adding contract support framework to C++ is to enable the programmers to define in a formal way what constitutes a contact violation (and therefore a bug) in their programs. This information can be later used by different tools to perform static or dynamic analysis of the program, add instrumentation code, or generate documentation or programmer hints in the IDE. It has been described in more detail in [P2388R4]. We want contracts to be available in freestanding implementations.

The motivation for producing this paper is to focus on documenting the consensus of SG21.

2. Notation {not}

Because the choice of syntax for contract annotations has no consensus yet, in this paper we use placeholder notation:

int select(int i, int j)
  PRE(i >= 0)               // precondition
  PRE(j >= 0)
  POST(r: r >= 0)           // postcondition; r names the return value
{
  ASSERT(_state >= 0);      // assertion; not necessarily an expression

  if (_state == 0) return i;
  else             return j;
}

3. Proposed characteristics {pro}

3.1. Three declarations: preconditions, postconditions and assertions{pro.tri}

We propose that all three types of declarations are included in the minimum contract support:

  1. Preconditions.
  2. Postconditions.
  3. Assertions.

Although it is possible to add only preconditions to the language and gain some benefit, we believe that only the three components added together bring sufficient value to warrant the modification of the language. We also believe that the syntax and semantics of preconditions must be compatible with these of the postconditions. So even if the preconditions were to be added in isolation, we would have to have a polished design for postconditions. This means that preconditions are blocked on the postcondition design even for the "only preconditions" variant.

The corresponding SG21 poll on 2021-12-14:

Poll: Postconditions should be in the MVP at this time.

SFFNASA
17341

3.2. Two translation modes{pro.mod}

We propose that there are two modes that a translation unit can be translated in:

  1. No_eval: compiler checks the validity of expressions in contract annotations, but the annotations have no effect on the generated binary. Functions appearing in the predicate are odr-used.
  2. Eval_and_abort: each contract annotation is checked at runtime. The check evaluates the corresponding predicate; if the result equals false, the program is stopped an error return value.

Too many modes are not necessary for the minimum contract implementation. The No_eval is required to provide no-overhead guarantee. The Eval_and_abort is required, because if we only had No_eval mode, users could start using contract annotations as (syntax-checked) comments, and might forget that these should always evaluate to true in the correct programs.

Can different translation units be translated in different modes? If we allowed it, we would have to answer questions like, what happens when the header file with the following contents is #included in two translation units:

inline void f(int i)
{
  ASSERT(i != 0); // which translation mode?
}

We do not want to prevent the implementations from enabling the "mixed mode" if they know how to answer the questions like the one above. At the same time, we do not want to force the implementaitons to offer the mixed mode. We also do not want to force them to diagnose the "mixed mode" situations, as this may not be easy or practical. Therefore, we propose for the MVP that the translation of different translation units in different modes in one program is ill-formed, no diagnostic required. This guarantees that the MVP is reasonably small an implementable, and leaves maximum freedom for the future additions. Ideally, we would also like to encourage the implementaitons to inform the programmers whether they support the mixed mode or not.

3.3. Evaluation order{pro.ord}

We propose the following evaluation order for preconditions and postconditions when a function is invoked.

  1. Function parameters are initialized.
  2. Preconditions are evaluated.
  3. Evaluation of the function body begins. (This includes constructor initialization list, function-try-block.)
  4. The return value, if any, is produced, creating an object in the caller or through the temporary materialization.
  5. The destructors of automatic objects are called.
  6. The postconditions are evaluated. (The postcondition can already see the returned object, and still see the function parameters.)
  7. The destructors of function parameters are called.

In this proposal throwing from the contract predicate triggers a call to std::terminate(), therefore there is no way to observe whether preconditions and postconditions are called inside or outside the function.

3.4. Name look-up{pro.lok}

We propose that names referred in preconditions and postconditions are looked up as if they appeared in a decltype in a trailing-return-type, if the function had one. In particular, this means that private members can appear in pre/post-conditions.

Programming guidelines often recommend that in contract predicates of public member functions one should only use the public interface of the class. This is to enable the user of the class to check the precondition in case the object state is not known. However, this is only a guideline, and enforcing it in the language would break other use cases that do not subscribe to the above advice. Also, precondition checks on member functions may be impossible to write using the public interface of the class because the contracts of the accessors might lead to recursive contract checks even when accessors themselves are not recursive.

In general, the users must ensure that the precondition of the called function is satisfied. If they do that, they do not have to check the precondition.

Allowing the access to protected and private members enables a practical usage scheme. In general, function precondition is something that cannot be fully expressed as C++ expression. The implementers choose how much of the function precondition they want to check. They may choose to check some parts of the precondition by accessing private members that they do not want to expose to the users, for instance, because the private implementation may change over time or under configuration:

class callback
{
#if !defined NDEBUG
  mutable int _call_count = 0;
#endif

  // ...

public:
  void operator() const
    // real contract: this function can be called no more than 8 times,
    // so the precondition is that the function has been called 7 or less times

#if !defined NDEBUG
    // attempt to check the precondition
    PRE(_call_count <= 7);
#endif
};

In the above example, the precondition can only be checked in debugging mode. Once NDEBUG is defined, member _call_count is removed and there is no way to test the precondition.

Also, a hypothetical constraint to use only public members in contract predicates could result in programmers turning their private and protected members into public members only to be able to express the pre- and postconditions, which does not sound like a good class design.

This has been described in detail in [P1289R1], and in fact adopted by EWG.

3.5. Naming the return value {pro.ret}

It is possible to name the return value (or reference) in the postcondition, except for one situation: when we use a return placeholder type and do not provide the definition from which the type could be deduced:

auto get_digit()
  POST(c: is_digit(c)); // error: decltype(c) unknown

This has been discussed in detail in [P1323R2].

3.6. Indirect function calls {pro.ptr}

Function pointers and references cannot have contract annotations, but functions with contract annotations can be assigned to them:

using fpa = int(*)(int) PRE(true); // error

using fptr = int(*)(int);
int f(int i) PRE(i >= 0);

fptr fp = f;  // OK
fp(1);        // precondition is checked in Eval_and_abort mode

In other words, contract annotations are not part of function type. This allows dynamically selecting behavior at runtime based on inputs.

int fast(int i) PRE(i > 0);  // fast, but has a narrow contract
int slow(int i) PRE(true);   // wide contract, but slow

int f(int i)
{
  int (*fp) (int) = i > 0 ? fast : slow;
  return fp(i);   // if fast() is called, its precondition is checked
}

The consequence of allowing this behavior is that an implementation cannot check the precondition at the call site for indirect calls. The check has to be performed either inside the function or in a thunk.

We propose the same behavior, for the same reasons, for function wrappers:

using fp = int(*)(int);
int f(int i) PRE(i >= 0);

function<int(int)> fp = f;  // OK
fp(1);   // precondition is checked in Eval_and_abort mode

3.7. Virtual functions {pro.vir}

Contract annotations may appear in virtual member function declarations, but only in non-overriding functions. When a virtual function is overridden, the overriding function has implicitly the same set of preconditions and postconditions as the overridden function, the program is ill-formed if you try to declare contract annotations in the overriding function explicitly, even if they look identical to the ones in the overridden function.

struct Base {
  virtual void f() PRE(p1());   // ok: introducing the precondition
};

struct Deriv1 : Base {
  void f() override;            // ok: Deriv1::f has precondition p1()
};

struct Deriv2 : Base {
  void f() override PRE(p1());  // error: Deriv2::f has the precondition redeclared
};

struct Deriv3 : Base {
  void f() override PRE(p2());  // error: Deriv3::f has different precondition than Base
};

The overriding function has the same contract annotations as the virtual function in the base class, and the names in the predicates are looked up in the context of the base class.

static const int N = 1; // #1

struct Base
{
  virtual void f() PRE(N == 1);
};

template <int N>       // N is shadowed
struct Deriv : Base
{
  void f() override;
};

int main()
{
  Deriv<2>{}.f(); // precondition test passes
}

The precondition in the overriding function is N == 1, but the name lookup is performed in the context of class Base, so it sees the global variable N declared in line #1.

If a predicate in the contract annotation of function f contains a call to a virtual function, the virtual function call is resolved as if the function was called inside function f:

struct Window 
{
  Window() POST(isClosed());
  virtual bool isClosed() const;
  virtual void open() PRE(isClosed());
}; 

struct SpecialWindow : Window
{
  bool isClosed() const override;
  void open() override;
};

int main()
{
  SpecialWindow w {}; // calls Window::isClosed(), because virtual function calls are not resolved in constructors 
  w.open();           // calls SpecialWindow::isClosed(), because isClosed is virtual
}

As a consequence of the above decsions, we do not allow the preconditions in the overriding function to be "wider" and the postconditions to be "narrower" than in the overridden function, even though this idea — one aspect of the Liskov Substitution Principle — is well explored and implemented in other languages. The reason for this is that we do not yet have a good understanding of what effect this principle should have on the feature design. Should it be just a "best practice" that the programmers are taught? Or should it be enforced by the language? But how? We could think of a number of ways. Given the declarations:

struct Base {
  virtual void f() PRE(p1());
};

struct Deriv : Base {
  void f() override PRE(p2());
};
  1. Should compiler be able to prove (even if it cannot see the definitions of p1 and p2) that the latter is no stricter than the former?
  2. Shall the compiler report an error unless the precondition in the overriding function has the form p1() || p2()?
  3. Or should the compiler accept this code and evaluate p1() && p2() when Deriv::f is called through the Base interface, but evaluate predicate p2() when Deriv::f is called directly?

Option 1 is clearly impossible. The other options might be implementable, but it is more like a guess, as we know of no implementation experience with these.

However, the decision to add support for this feature can be deferred for later, because the way we specify the feature now (ill formed) remains open for future extensions in any of the three directions.

3.7.1 Class templates {pro.vir.tmp}

The same restrictions for virtual functions apply for class templates, except that compilation errors might be deferred till template instantiation time:

struct Base1 {
  virtual void f1(int i);
};

struct Base2 {
  virtual void f2(int i);
};

template <typename Base>
struct Deriv : Base {
  void f2(int i) PRE(i > 0); // ok, so far
};

Deriv<Base1> d1 {}; // ok
Deriv<Base2> d2 {}; // compiler error

3.7.2 Inheriting multiple contracts {pro.vir.two}

In case a member function overrides two functions from two base classess with possibly two different set of pre- and postconditions, its precondition is the logical conjunction of the preconditions in the overridden functions, and it postcondition is the logical conjunction of the postconditions in the overridden functions:

struct Base1 {
  virtual void f(int i) PRE(p1()) POST(r1());
};

struct Base2 {
  virtual void f(int i) PRE(p2()) POST(r2());
};

struct Deriv : Base1, Base2 {
  void 2(int i) override
    // inherited:
    // PRE(p1()) PRE(p2()) POST(r1()) POST(r2())
  ;
};

3.8. Contract annotations and the immediate context {pro.imm}

In this proposal the predicates in contract annotations are not in the immediate context of the function. They behave similarly to exception specification:

template <std::regular T>
void f(T v, T u)
  PRE(v < u); // not part of std::regular

template <typename T>
constexpr bool has_f =
  std::regular<T> &&
  requires(T v, T u) { f(v, u); };

static_assert( has_f<std::string>);         // OK: has_f returns true
static_assert(!has_f<std::complex<float>>); // ill-formed: has_f causes hard instantiation error

As a consequence, we may have a function template that works well for a given type, but stops working the moment we add a contract annotation. This also affects how concepts would be taught: a good concept should express not only the requirements that are necessary in the implementation of the generic algorithms, but also those that are necessary in the specification of contract annotations in these algorithms.

3.9. abort() vs terminate() {pro.end}

In this proposal, throwing from the predicate calls std::terminate() while a failed runtime check aborts the application even more abruptly: close to calling std::abort(), but we do not require the actual call to std::abort(), as the function may not be present in freestanding.

We do not require the implementations to allow the users to install custom contract violation handlers, nor do we specify any interface describing how this is done. However, we do not actively forbid the implementations form performing some logic, as long as it never throws or calls longjmp(). This makes the MVP proposal smaller; but it remians open for the contract violation handler support in the future.

The above distinction reflects the fundamental difference between the two situations. Throwing from a predicate is analogous to throwing from a noexcept function — an expected response to an unhandled exception thrown in procedural code — but it does not signal that the program state itself is corrupt, or that the program has a logic error, which is what a contract violation detects. Maybe a comparison had to allocate memory, and this allocation failed, because today the server is exceptionally busy. We want to handle it the way we usually handle exceptions when there is no suitable handler: std::terminate() is an exception handler, with its unique control flow, however harsh.

In contrast, failing a runtime correctness test is an indication of a bug, and it is not clear if std::terminate(), which is the second level of exception handling mechanism, is a suitable tool. The call to std::terminate() either calls std::abort() or calls a terminate handler installed by the user. In case the contract is violated, and we can be sure the program contains a bug, calling a user-installed function may be unsafe, and can pose a security risk.

Moreover, std::terminate() is not available in freestanding implementations.

3.10. No runtime error message{pro.log}

This revision of the paper does not require or encourage any error message to be displayed to standard diagnostic stream, or anywhere in Eval_and_abort mode. There are two reasons. First, there is no standard diagnostic stream on freestanding implementations, and we want contract support to be available on those platforms. Second, for security reasons. When an application is in a confirmed incorrect state, performing IO operations may pose a security risk. As the primary focus of this proposal is safety, we choose a conservative approach.

Note that breaking into a debugger upon contract violation is a valid way to handle these situations, as it takes a single instruction and does not depend on program state.

3.11. Contract annotations upon the first and subsequent declarations{pro.dec}

We require that if a given function f has declared preconditions and postconditions, they shall be visible in the first declaration of f in a translation unit (TU): otherwise the program is ill-formed. Subsequent declarations must omit contract annotations. If f is declared in more than one TU, the corresponding first declarations of f shall be identical (modulo parameter names): otherwise the program is ill-formed with no diagnostic required. As a consequence, the following is illegal:

int select(int i, int j);  // first declaration
	
int select(int i, int j)   // second declaration
  PRE(i >= 0)              // error: initial decl has no contract annotations
  PRE(j >= 0)
  POST(r: r >= 0); 

The following is also illegal

int select(int i, int j)  // first declaration
  PRE(i >= 0)
  PRE(j >= 0)
  POST(r: r >= 0);
	
int select(int i, int j)   // second declaration
  PRE(i >= 0)              // error: contract annotations on redeclaration
  PRE(j >= 0)
  POST(r: r >= 0); 

The reason for this restriction is implementability issues, similar to those for default function arguments. This decision departs from [P0542R5], which allowed putting odr-identical contract annotations on redeclarations. The reason we do not allow contract annotations on redeclarations is because this way we avoid the reason to define the notion of being "odr-identical".

3.12. Non-reference parameters mentioned in postconditions must be const{pro.arg}

If a non-reference function parameter is named in a postcondition, that parameter shall be declared const in every declaration of the function.

int generate(int lo, int hi)              // error: lo and hi should be declared const
  PRE(lo <= hi)
  POST(r: lo <= r && r <= hi);
	
int generate(int& lo, const int& hi)      // ok: lo and hi are references
  PRE(lo <= hi)
  POST(r: lo <= r && r <= hi);
	
int generate(int lo, int hi)              // ok: lo and hi not referenced in a postcondition
  PRE(lo <= hi)
  POST(r: r >= 0);
	
int generate(const int lo, const int hi)  // ok: lo and hi are declared const
  PRE(lo <= hi)
  POST(r: lo <= r && r <= hi);

This is to prevent the situation where a contract check would return an answer incompatible with the programmer expectations: a false positive or a false negative. This problem has been explained in detail in [P2388R4] and [P2466R0]. Here, we only show an example that demonstrates the issue:

// declaration that the user sees:
int generate(int lo, int hi)
  PRE(lo <= hi)
  POST(r: lo <= r && r <= hi);

// definition that only the author sees:
int generate(int lo, int hi)
{
  int result = lo;
  while (++lo <= hi) // note: lo modified
  {
    if (further())
      ++result;      // incremented slower than lo
  }
  return result;     // at this point result < lo
}

// usage:
int min = 1;
int max = 10;

int r = generate(min, max);   // postcondition check fails
assert(min <= r && r <= max); // even though this assertion is satisfied

How is this problem addressed in other languages? In D, this problem has been ignored: postconditions like the one above give false positive or false negative results. In ADA this problem does not occur: this is due to the way the function arguments are designed. In ADA, for each function argument, the programmer has to specify if it is IN or OUT or INOUT. The OUT and INOUT parameters correspond to reference parameters in C++, so there is no problem here. The IN parameters, on the other hand, are immutable, so there is no question of changing them inside the function: IN parameters correspond to const by-value parameters in C++. SG21 decided to follow what ADA does, in the following poll on 2022-03-10.

Poll: Adopt a change based on option #2 from the paper [P2521R1] section 4.3: if the postcondtion uses a non-reference parameter: require it to be const objects.

SFFNASA
56010

This decision has the following consequences. First, in the MVP contracts, the programers have the following options when they need their postconditions to refer to non-reference function parameters:

  1. Do not reflect this postcondition in a contract annotation. (Do what you do in C++20, put it in a comment...)
  2. Add the otherwise redundant const qualifier.

Second, this implies that once a postcondition starts referencing a non-reference function parameter, the language rules that govern this parameter change: now the additional const qualifier makes a difference: programmers can no longer choose to add it or omit it between declarations:

void f(int i) POST(i != 0);       // error: i must be const 

void g(const int i) POST(i != 0);
void g(int i) {}                  // error: missing const for i in definition

void h(const int i) POST(i != 0);
void h(const int i) {} 
void h(int i);                    // error: missing const for i in redeclaration

This choice guarantees that compiler statically prevents any modifications to these functin parameters: both in the function body and in the contract predicates:

void f(const int i) 
  POST(++i != 0)                 // error: cannot mutate a const object
  POST(is_const_v<decltype(i)>); // postcondition satisfied

void f(const int i)
{
  ++i;                           // error: cannot mutate a const object
}	

One consequence of this is that you cannot use move-semantics for function parameters referenced in postconditions:

void f(unique_ptr<int> i) 
  PRE(i)                        // ok (no restrictions for preconditions)
{
  return i;                     // ok: move
}

void g(const unique_ptr<int> i) // const is now required 
  PRE(i)              
  POST(i)
{
  ++*i;
  return i;                     // error: copy constructor inaccessible
}

This price is paid even if the programmer uses only No_eval mode. For copyable types with efficient move, this may mean turning some moves into copies:

string f(const string s) // `s` is const because the first declaration of `f()` has a postcondition
{
  // long function body that only reads `s`
  return s;              // copy, used to be a move 
}

This is arguably inconvenient, however this remains within the normal rules of C++: if an object is declared const then in cannot be moved-from. It sould be noted that, for the scope of MVP, the only viable alternative is to make postconditions that refer to non-reference function parameters invalid. For the post-MVP future the planned solution is for the user to request that copies of function arguments be done on the side, as described in section {con.syn.arg}.

The additional const qualifier still does not affect the type of the function:

int f(const int i) 
  POST(r: r != i);

int (*fp)(int) = &f; // ok

3.12.1 Can the problem be avoided by inspecting function arguments instead?{pro.arg.out}

It has been suggested that the problem with function parameters referenced in postconditions could be avoided if we checked the values of function arguments used to initialize the function parameters, instead of checking the parameters themselves:

int f(int i) POST(r: r != i);

int a = 1;
int b = f(a); // in postcondition read value of `a` rather than value of `i`

This idea will not work for more complex cases, unless a copy of the argument is made on the side. First, you cannot assume that the value of the argument remains unchanged as the function is executed, due to aliasing problem.

int f(int a, int& ref)
  POST(r: r != a)
{
  --ref;
  return a - 1;
}

int i = 1;
f(i, i);   // at the end of f(), `i` has different value than `a`

Another problem with the proposed idea is that we may not have the function argument of the same type as the function parameter:

string f(string s)
  POST(r: s.empty() || r == s);

auto x = "text"; // type of `x` is `const char*`
f(x);            // cannot call `x.empty()`

4. Controversial aspects {con}

This section lists points of controversy inside SG21 for the recent contract design. For each of these points, we require a poll to be taken, to determine the group direction.

4.1. The choice of syntax{con.syn}

There are two visions for the syntax to describe contract annotations with significant support in SG21.

One is to use notation similar to attributes (but not 100% compatible with attributes):

int select(int i, int j)
  [[pre: i >= 0]]
  [[pre: j >= 0]]
  [[post r: r >= 0]]      // r names the return value
{
  [[assert: _state >= 0]];

  if (_state == 0) return i;
  else             return j;
}

The other is to use notation similar to lambdas (but not 100% compatible with lambdas):

int select(int i, int j)
  pre{ i >= 0 }
  pre{ j >= 0 }
  post(r){ r >= 0 }      // r names the return value
{
  assert{ _state >= 0 };

  if (_state == 0) return i;
  else             return j;
}

The rationale for using the later syntax has been provided in [P2461R1]. The analysis of pros and cons of using the former syntax has been provided in [P2487R0].

The primary argument in favor of quasi-attribute notation is to stress semantic characteristics similar to attributes. The common understanding of attributes is that they are hints for generating warnings or performing optimizations. Their removal should not affect the correctness of the program (even though it is easy to construct an example using no_unique_address that contradicts this claim).

Contract annotations — at least one model thereof — shares similar features: they are hints for tools for generating warnings or emitting an instrumentation code. If these annotations are removed from a correct program (one that does not violate the declared contract annotations), this does not affect the correctness of the program.

The primary arguments in favor of quasi-lambda syntax is to avoid the problems reported for quasi-attribute syntax (e.g., that they look like attributes but do not follow other characteristics of attributes) and to offer an intuitive syntax for one of the future extensions: making copies of function arguments for use in postconditions.

4.1.1 The capacity to copy function arguments (post MVP){con.syn.arg}

This section describes a future extension, not proposed for the MVP: the ability to make copies of function arguments (or parts thereof) upon user request, to be later referenced in postconditions. However, the capability to handle this extension is related to the choice of syntax.

[P2461R1] proposes the following syntax:

int generate(int lo, int hi)
  pre{ lo <= hi }
  post[lo, hi](r){ lo <= r && r <= hi }; // `hi` and `lo` refer to internal copies of function parameters.

The lambda-introducer syntax should make it immediately clear, even for the uninitiated programmers, that a copy of function parameters is being made.

The quasi-attribute notation also allows this as a future extension, however this would require a new notation, which comes with a complexity and an aesthetical cost:

int generate(int lo, int hi)
  [[pre: lo <= hi ]]
  [[post r, old_lo = lo, old_hi = hi: old_lo <= r && r <= old_hi ]];
	
// or some alternate notation

int generate(int lo, int hi)
  [[pre: lo <= hi ]]
  [[post r, =lo, =hi: lo <= r && r <= hi ]];
	
// or a notation using lambda-capture:

int generate(int lo, int hi)
  [[pre: lo <= hi ]]
  [[post [lo, hi] r: lo <= r && r <= hi ]];

Thus, the decision how to address the issue of by-value arguments in postconditions is somewhat tied to the choice of syntax. But perhaps not as much as one might think at first.

It should be noted [P2461R1] offers more motivation than the quasi-lambda syntax than solving the problem of function arguments in postconditions. The notable exmple is the support for "oldof" values:

void vector::push_back(T const& val)
  POST(r: size() == OLDOF(size()) + 1);
	
// in P2461R1, post-MVP:

void vector::push_back(T const& val)
  post [old_size = size()]{ size() == oldof_size + 1 };

// in P2388R4, post-MVP:

void vector::push_back(T const& val)
  [[post old_size = size(): size() == old_size + 1]];
	
// or:

void vector::push_back(T const& val)
  [[post [old_size = size()]: size() == old_size + 1]];

4.2. Removal and duplication of side effects in predicates{con.eff}

Some implementation strategies may need to evaluate the same predicate in a precondition twice. For direct function calls, an implementation can easily insert the instrumentation code in the caller. This is desired as it gives better diagnostics. However, this is impossible when a function is called indirectly, either through a pointer or std::function: from the pointer signature we do not know if a function called has a precondition or not. To address that case, one thing an implementation could do is to compile the pre- and post-condition checks into the function body. This would give the result that the pre-/post-conditions are checked normally when the function is called through an indirection, but are checked twice when the function is called directly: once in the caller, and once inside the function body. We may want to enable such implementation strategies. The consequence for the programmer is that when the predicate has side effects, these effects occur twice.

Putting side effects in contract annotaitons and later relying on them is a practice that we would like actively discourage. As of today, we do not know how to do it statically (so that each such side effect would be reported as a compiler error). For the purpose of discouraging programmers from putting observable side effects in their contract annotations, an implementation might want not to evaluate the predicate, if it already knows what its result would be. This can happen when a function that produces a value has sufficiently similar postcondition p to the precondition of another function that subsequently consume the same value, and we do not see the body of p:

bool p(int); // defined in a different TU

int produce() POST(r: p(r));
void consume(int i) PRE(p(i));

int main() {
  consume(produce()); // can p() be called once
}

This seems redundant to call the same predicate twice. Of course, this seems so only if p() doesn't have side effects. If it does, and the program (or the programmer) relies on them, this elision can make the comprehension of the program harder, and the effects surprising.

Both [P2388R4] and [P2461R1] propose this capability to remove and duplicate the evaluation of the predicates. However, concerns have been expressed about it.

Note that [P2388R4] additionally proposes the "partial elision" of side effects in a predicate. We received a feedback that the group is against it, so this "partial elision" is not considered in this paper.

5. Acknowledgements {ack}

This paper is a summary of SG21 discussions; all SG21 members contributed to this paper. John McFarlane suggeted the idea to make implicit copies of trivilly-copyable types. Walter E. Brown pointed out that putting pre-/post-condition checks inside function bodies is not a necessity, and that alternate implementations — such as a thunk — exist.

6. References {ref}