<html>
<head>
<title>Value constraints</title>
</head>
<body>
<p>Author: Andrzej Krzemieński</p>
<h1>Value constraints</h1>
<p>In this paper we want to analyse how a support for contract programming-like features could be supported in C++. We use a different term "value constraints" to stress that we do not necessarily want to copy solutions that other imperative programming languages adapt. We want to change the focus from how broken contracts are responded to in run-time, to how contract violations can be detected at compile-time. This is a high-level overview of the problem, and we are not even covering the things like sub-contracting or other interactions with OO features.</p>
<h1>Comparison with other contract-programming proposals</h1>
<p>While <a href="#N1962">[N1962]</a> is a fairly complete proposal for adding contract-programming support to C++, this document offers an analysis of the problem domain rather than making a specific proposal. We focus on identifying expectations, potential implementation difficulties and costs.</p>
<p>All other contract programming proposals that we are aware of — <a href="#N4075">[N4075]</a>, <a href="#N4110">[N4110]</a> — start from the assumption that the support for preconditions must be provided in the from of evaluating preconditions before function calls, occasionally disabling these precondition evaluations, and installing broken contract handlers. In this paper, we do not take this assumption for granted. Run-time support is only a subset of the scope of our analysis. We explore in more detail an alternative approach: the focus on static analysis (also indicated in <a href="#N1962">[N1962]</a>).</p>
<h1>What do we need?</h1>
<p>
The 'features' we describe here can be collectively called <em>value constraints.</em>
We want to use them to express in the language that certain combinations of values of certain objects
at certain times are invalid and are intended (and expected) never to occur.</p>
<h2>Specify function's domain</h2>
<p>The problem goes back to mathematics. Certain functions are well defined
only for a subset of values of the input type. For instance, a square root
returning real numbers is not defined for negative numbers.
What does it mean for a function in a programming language like C++
that it is not defined? Currently there are two approaches. One is to detect
the value of the parameter(s) that the function should not be prepared for
and execute a different logic: returning a special value, throwing an exception, etc.
Using our example with a square root, a corresponding function <code>sqrt()</code>
could be defined as follows:</p>
<pre>double sqrt(double x)
{
if (x >= 0.0) {
//<em> do proper algorithm</em>
}
else {
return numeric_limits<double>::signaling_NaN();
// <em>or throw an exception</em>
}
}
</pre>
<p>What it effectively does is to change the function's domain. Now the functions do not restrict its domain anymore.
It is well defined for every value of an input type, and does other things than only the "proper algorithm".
This has an unintended consequence: our function can be used for detecting negative numbers:
</p>
<pre>double is_negative(double x)
{
return isnan(sqrt(x));
}
</pre>
<p>Another way of approaching the function domain problem is to informally 'announce' that the function is not
defined for certain values of input types and implement it with the assumption that the undesired values
are never passed to the function:</p>
<pre>
double sqrt(double x)
// requires: x >= 0.0
{
// proper algorithm:
double y = 1.0;
double prev_y;
do {
prev_y = y;
y = (y + x / y) * 0.5;
}
while (!closeEnough(y, prev_y));
return y;
}
</pre>
<p>This uses Newton's Iteration algorithm. The loop will terminate when values <code>y</code> and <code>prev_y</code> become close enough. They will only do that when <code>x</code> is non-negative. Supplying a negative value will make the loop run forever and hang the program. Another adverse effect of supplying an argument the function is not prepared for is an undefined behaviour (e.g., when providing a too large index to <code>vector::operator[]</code>). Another is the risk of function returning a result that has no meaningful interpretation.</code><p>
</p>Note that in the example above even a clever analyser is unlikely to detect from the function body that passing a negative input to this function is something wrong. Thus we cannot say that checking such condition is only the Quality-of-Implementation issue. But everything is fine as long as no negative number is passed in. 'Announcing' that the function is not prepared for just any input is informal: it is either written in the comment, or in paper or html documentation, or only spread by word, or assumed to be obvious. This risks an unintended negative program behaviour, like a halt, or an undefined behaviour. However, it is often preferred because of performance and inability to come up with a reasonable fall-back action. Consider <code>std::vector::operator[]</code>, it does not check the bounds for performance reasons. If it was used in the following code:</p>
<pre>
for (int i = 0; i != vec.size(); ++i) {
if (i > 0) cout << ", ";
cout << vec[i];
}
</pre>
<p>The condition in the loop already checks if the index is within bounds. If <code>operator[]</code> was also checking the same condition inside, we would be wasting time on doing redundant checks. Also, for some functions it is not possible to think of any fall-back action. For instance <code>std::vector::swap</code> must not throw exceptions and returns <code>void</code>, yet, it is not well defined when two vectors' allocators do not compare equal.</p>
<p>Not checking for argument being within domain and delegating the check to the callers is desirable, especially that the caller is in a better position in verifying if the domain of the function. Consider:</p>
<pre>return sqrt(abs(x));</pre>
<p>The caller can be sure that no negative value is passed to function <code>sqrt()</code> even though no check is performed at all. Function domain defined this way is a <em>contract</em> between function author and function callers. The author defines the domain and assumes he will not get values from outside the domain. The caller guarantees that she will not pass values outside the domain. Out of all contracts described here, this one is the most likely to be broken, because it is the only one where the person responsible for guaranteeing is different than the person declaring the contract. The user may not be aware that a function has requirements on the values of parameters, or may misunderstand what the requirement is. Therefore this contract requires the most serious attention and support in the language.</p>
<p>What we need is the ability to declare the function's domain along with the function, so that it is visible to the callers and to the automated tools. How the tools can handle this is a secondary issue, but the behaviour can be: (1) automated documentation generation, (2) additional warnings from static analysers, (3) additional instrumentation injected by compilers, (4) compiler optimizations based on domain declarations, (5) the standard can adopt this notation to more formally specify its preconditions.</p>
<h2>Specify function's range</h2>
<p>Here, we use term 'range' in the mathematical sense: the set of all possible values that the function can return (a subset of function's co-domain). In the above example with function <code>abs()</code>, a hypothetical tool could detect that expression <code>sqrt(abs(x))</code> is always fine only if it knew that the range of <code>abs</code> is equal (or smaller) than the domain of <code>sqrt</code>. We need to be able to constrain the allowed function output in order for automated tools to be able to verify if other functions' domain requirements are satisfied. </p>
<p>In this case a function author specifies the contract and (likely) the same author guarantees it. Function's user can rely on the guarantee. It is much less likely that this contract is broken, because it is the same person that declares and later ensures the obligation. And conversely, if the author makes an error in the function, he is equally likely to make an error in specifying the contract.</p>
<h2>Block-level assertions</h2>
<p>This type of value constraint is quite familiar to many C++ user, as it is implemented with macro <code>assert</code> and some similar tools in many libraries. If we think of it as a contract, this time a function author defines it, he ensures that it holds, and he is the benefactor of the contract: he guarantees something to himself, namely that certain state of a block-local variable or set of variables shall never occur at the point of the assertion. At the same time the function author guarantees something that he can be held accountable for, and relies on the guarantee expressed with the assertion.</p>
<h2>Class-level assertions</h2>
<p>A similar constraint on variables is often required for (non-static) data members of objects of a given class. Consider the following example:</p>
<pre>class WeighedAverage
{
double wgt1_ = 0.5;
double wgt2_ = 0.5;
public:
double average(double val1, double val2) const;
<em>// ensures: answer is between val1 and val2</em>
{ return wgt1_ * val1 + wgt2_ * val2; }
void set_1st_weight(double w1);
<em>// requires: w1 between 0.0 and 1.0</em>
{ wgt1_ = w1; wgt2_ = 1.0 - w1; }
<em>// always true: wgt1_ between 0.0 and 1.0</em>
<em>// always true: wgt2_ between 0.0 and 1.0</em>
<em>// always true: wgt1_ + wgt2_ == 1.0</em>
};
</pre>
<p>Note the three comments at the bottom. They are something that could be expressed with macro <code>assert</code>, except that <code>assert</code> is an expression and cannot be put at the class scope. Note also that members <code>wgt1_</code> and <code>wgt2_</code> are private. So, we are not declaring anything to the outside world. Word "always" needs to be more formal. It applies to any object of this class whose life time has begun and have not yet ended, except that member functions can temporarily compromise it provided that they restore it upon exit (either via exception or a normal return). Also, in case of thread or context switching, if a function decides to temporarily break such class-scope assertion, it must guard this action with a lock or equivalent, so that other threads do not see an object with a broken contract.</p>
<p>Class-level assertions (or class invariants) could be used as a criterion for good abstractions, much like axioms in concepts. If you cannot specify an invariant, it might be an indication that the design/abstraction may be poor or this should not have been made a class.</p>
<h2>Specify equivalent expressions</h2>
<p>Often library interfaces offer more than one way of doing the same thing. For instance, checking if a container contains at least one element can be checked in two ways: <code>cont.empty()</code> and <code>cont.size() != 0</code>. The latter is more general and could be used to check for emptiness, but there are occasions where the former can execute faster. This justifies the existence of the two forms. However, the job of matching one function's domain with other function's co-domain would be severely impeded if either specified the contract with a different (albeit equivalent) expression. Consider:</p>
<pre>template <typename T>
class vector
{
void resize (size_t s); <em>// ensures: this->size() == s</em>
const T& front() const; <em>// requires: !this->empty()</em>
};
vec.resize(1);
return vec.front(); <em>// safe?</em>
</pre>
<p>Can we match what <code>resize</code> guarantees with what <code>front</code> expects? The two expressions are different. It would be much easier if we were able to explicitly declare that for any <code>std::vector</code> expressions <code>vec.empty()</code> and <code>vec.size() != 0</code> are equivalent. This is somewhat similar to class-level assertions, but the declaration applies to more than one class, now we are only interested in the public interfaces, and we can express equivalence between expressions that have side effects. for instance, we can specify that <code>vec.clear()</code> is equivalent to <code>vec.resize(0)</code>. Out of all "constraints" described in this section, this is the only one where term "value constraint" is inadequate. This is a constraint on the semantics of expressions. But we need it for the automated tools to make an effective use of other value constraints.</p>
<h2>Loop variants</h2>
<p>Note that this is not the same as loop <em>invariant</em> (which can be handled by a block-level invariant). This is somewhat similar to an assertion. It can help convince oneself that a non-trivial loop will ultimately terminate. Sometimes it is not easily seen, because there is no loop counter. We may for instance inspect elements in the collection by skipping some elements, increasing or shrinking, the collection. A loop variant is an expression that evaluates to an integral non-negative number. It is expected that in each loop iteration evaluating this expression renders a number smaller than in the previous iteration. It is also expected that when the value renders zero, the loop terminates.</p>
<p>A framework for supporting value constraints need not address all the above needs. We believe that only supporting the declaration of function domain is a big help in itself. Note that while assertions loop variants need to work with expressions, the features for specifying function domain and co-domain need not necessarily use expressions. We address this in detail in the later sections.</p>
<h1>What use can be made of value constraints?</h1>
<p>Value constraints exist, even though there is no language support for them in the language. We have seen in the above examples that comments were used to convey the information. In this section we list the benefits obtained form standardizing or formalizing value constraints this way or the other.</p>
<p>In order for an automated tool to understand the constraint, we have to provide a special-purpose syntax. Some tools expect that it is put inside source code comments. For instance <a href="#ACSL">[ACSL]</a> uses the following notation: </p>
<pre><em>/*@ requires x >= 0;
ensures \result >= 0;
*/</em>
double sqrt(double x);</pre>
<p>But for structured comments like the above, C++ has an alternative: [[attributes]]. Attributes are akin to comments because they intended not to affect the semantics of correct programs. On the other hand they can be used as hints for optimizations, warnings and any kind of program analysis. If the expectation of value constraints is to affect the program behaviour, attributes will not do, and a special language feature would need to be devised.</p>
<p>An ideal — and unrealistic — support for value constraints is for compiler to check any possible flow in the program and signal a compiler error whenever a breach of the constraint is going to happen. Because this is not doable, the we aim at the support that is not entirely satisfactory, but believed to be better than none.</p>
<h2>Improved documentation</h2>
<p>One of the obvious uses of formalized value constraints is the automated generation of documentation. Even if developers do not use any tool for generating documentation, there is still a gain. When a developer sees the declaration of the function she is going to use, she can immediately see the value constraints as well. If they are a language feature, developers are more encouraged to use them (even though comments would do). Since this does not affect program semantics [[attributes]] are sufficient.</p>
<h2>Static analysis</h2>
<p>Value constraints could enable static analysers to detect a potential breach of value constraints and issue warnings. Again, using value constraints this way does not affect program semantics, so [[attributes]] would do.</p>
<h2>Constraint-based compiler optimizations</h2>
<p>In that case, compiler is able to arbitrarily change the behaviour of the program in case where a value constraint has been violated. So, adding a value constraint may change the meaning of the program. In this case attributes will not suffice, and we need a language extension for specifying value constraints.</p>
<h2>Auto-generation of runtime checks</h2>
<p>This is what Eiffel provides and what <a href="#N1962">[N1962]</a> proposes. Value constraints need to be C++ expressions. An implementation can (optionally) inject, at well defined places, a code that evaluates at run-time expressions representing value constraints. If any (boolean) expression evaluates to <code>false</code>, a certain action (like calling <code>std::terminate</code>) is performed. The insertion of additional logic requires that value constraints are introduced as a language feature. In fact even more language and library features is required to control when and how the run-time checks are performed and responded to.</p>
<h1>Run-time evaluation of value constraints</h1>
<p>In this section we focus on one possible approach: treating value constraints as expressions and evaluating them at run-time.</p>
<h2>Side effects of the expressions</h2>
<p>Using expressions with side effects in value constraints is generally discouraged, but sometimes it might be difficult to spot that we have a side effect. For the purpose of this discussion we also consider run-time overhead, and especially the run-time complexity as a side effect. To minimize the possibility of invoking a function with a side effect <a href="#N1962">[N1962]</a> proposes that only <code>const</code>-qualified member functions are allowed; but even these can modify non-member variables, and it is not only member functions that may need to be used to express value constraints. Ideally, we would like to use only <em>pure</em> (referentially transparent) expressions, but C++ as of today does not offer the possibility of detecting if an expression is pure. Although the definition of relaxed <code>constexpr</code> functions makes a step towards pure functions.</p>
<p>A practical question to be answered, given the syntax from <a href="#N1962">[N1962]</a>, is if the following to be a legal code for detecting if run-time value constraint checks are enabled?</p>
<pre>
int preconditions_on = false;
void test() precondition{ preconditions_on = true; }
{
cout << "preconditions are on: " << preconditions_on;
}
</pre>
<p>Note that we assign a new value to a global object in the precondition. One possible way to address this issue is to say that any modification to the program state in value constraints renders an undefined behaviour. Another is to say that this is correct a program, but the expression may or may not be evaluated. This makes it an unspecified behaviour.</p>
<p>And similarly, is the following a reliable way of checking if a number is negative?</p>
<pre>double sqrt(double x) precondition { x >= 0.0; };
double is_negative(double x)
{
set_precondition_broken_handler(&throw_exception);
try { sqrt(x) };
catch (exception const&) { return true; }
return false;
}
</pre>
<p>We probably do not want to encourage such contrived usages, but can this be expressed in the standard? If we say that it is unspecified whether value constraints are evaluated or not, we would make it clear that the code as above is not reliable. But then again, someone else may be disappointed that his precondition is not guaranteed to be checked.</p>
<p>If we consider value constraints with side effects an 'invalid' code, do we force the compiler to reject every such case with a diagnostic message? If it is impossible in the general case (and so it seams), we have to accept that such code is valid, but do we allow the compiler to reject these cases where it can prove that we have a side effect?</p>
<h2>Value constraints in overloaded functions</h2>
<p>Consider the following declaration:</p>
<pre>
template <typename InputIter>
void displayFirstSecondNext(InputIter beg, InputIter end);
<em>// requires: std::distance(beg, end) >=2</em>
</pre>
<p>Is function template <code>std::distance</code> referentially transparent? The answer is: it is not templates that can or cannot be pure but functions. Some functions instantiated from this template will be pure, others will not — it depends what iterator type the template will be instantiated with. Consider <code>InputIterator</code>. In the worst case (of <code>std::istream_iterator</code>) incrementing the iterator invalidates other iterators referring to the same stream. This is a tricky behaviour: by changing our internal copies of objects (iterators), we alter (invalidate) other, external objects. Function <code>std::distance</code> does increment iterators. If our precondition was to be evaluated, this might cause an undefined behaviour in the program.</p>
<p>Thus, we have an expression; it is pure and natural to use for some instantiations, and has severe side effects for other instantiations. We would like the predicate to be evaluated for forward iterators and never evaluated for other iterators. How do we want a concept-programming framework to address the cases like this one?</p>
<p>One option is to say "this case is special: you will not be able to express a precondition". Another is to require of the authors to provide two overloads: one for <code>InputIterator</code>s, the other for <code>ForwardIterator</code>s. They will do exactly the same thing except that one will have a precondition and the other will not. Note that you cannot just say "if the predicate is constant evaluate it otherwise don't evaluate it". In either case we take iterators by value. It is just that input iterators do not expose value semantics — this cannot be checked by the compiler.</p>
<p>The above case can be solved by introducing a yet another feature: an annotation that a precondition is only evaluated when some compile-time condition is met: in our case only if the iterator is a <code>ForwardIterator</code>. Note that one global switch (similar to <code>NDEBUG</code>) saying "disable/enable all value constraint evaluations" will not be enough.</p>
<h2>Inadvertent increase in run-time complexity</h2>
<p>There are other reasons for having a more fine grained control of which checks should be enabled. Consider a binary search algorithm. Its runtime complexity is O(log <var>n</var>). It has an obvious precondition that the range we search through is sorted. Performing the sorted check has complexity O(<var>n</var>). Thus by evaluating the precondition, we change the algorithms complexity. This might be unacceptable, even for some debug/testing builds. Runtime complexity is a sort of side effect of an algorithm, and it can be silently added to the function, especially when following a good practise a developer adds an obvious precondition, which would be his primary task, and forgets the secondary task of specifying (using some contract-specific sub-language) the conditions under which this precondition shall be evaluated.</p>
<h2>Run-time response to a broken contract</h2>
<p><a href="#N1962">[N1962]</a> as well as <a href="#N4075">[N4075]</a> propose that the action taken upon violating a value constraint should be configurable by the programmer. While we agree this should be configurable, we object to the way of achieving this by <code>std::set_terminate</code>-like registering function. Language allows that <code>std::set_terminate</code> can be called multiple times from multiple places: different, possibly dynamically-loaded/shared libraries. This makes sense for <code>std::terminate</code>. Every part of the system may acquire a <em>critical</em> resource: one that has to be released even if "exception handling must be abandoned for less subtle error handling techniques". In that case the component also needs to register an additional clean-up function. In case of broken contract situation, we do not need or want that flexibility. We believe only the person that assembles the final program from the components and libraries, should be empowered to to decide how broken contracts are handled. Only him does have the knowledge if this is a test or a retail build; if the slow-down of some run-time checks can be afforded. Libraries do not know that: they do not know in what environment they will be used.</p>
<p>Additionally, the <code>std::set_terminate</code> mechanism has a certain flow. Unless you apply some syntactic contortions, you cannot set the handler for functions executed before <code>main()</code>.</p>
<p>We are not aware of any mechanism currently available in C++ that would facilitate our needs. But since function <code>main</code> has the property of being required to be defined only once across the executable program, a solution we are leaning towards is to apply some special annotation around function <code>main</code> that would indicate what the user's preference is on the handling of broken contracts.</p>
<h2>What can a broken contract handler do?</h2>
<p>The most reasonable default answer appears to be <code>std::terminate</code>, which means "release critical resources and abort". One may wish to override the default in order to do special logging. We believe that it is not a good idea to throw from a broken contract handler. First, throwing an exception is often an action taken inside a function,in a situation where it cannot satisfy the postcondition, to make sure that class invariants are preserved. In other words, if you catch an exception or are in the middle of stack unwinding, you can safely assume that all objects' invariants are satisfied (and you can safely call destructors that may rely on invariants). If it were possible to throw from the handlers, his expectation would be violated. Also, you can imagine functions that are marked as <code>noexcept</code> and still impose a value constraint (which happens to fire). <a href="N4110">[N4110]</a> argues that "the exception can be safely thrown in this case (even if the function is <code>noexcept</code>) as it would be thrown in the caller side and not in the callee side". We disagreewith this reasoning. Consider this example:</p>
<pre>bool positive_predicate(int i) noexcept <em>/* requires: i > 0 */</em>;
bool predicate(int i) noexcept <em>/* requires: true */</em>
{
if (i < 0)
return negative_predicate(i);
else
return positive_predicate(i);
</pre>
<p>Now imagine that we make a call <code>predicate(0)</code>. Due to a bug in the function, we call <code>positive_predicate</code> with a broken precondition. It doesn't help that the throw from the handler is made from the context outside of function <code>positive_predicate</code>, because it is still made inside the caller function <code>predicate</code>, which is also <code>noexcept</code>.</p>
<p>The recommendations from <a href="N3248">[N3248]</a> (that functions with narrow contract should not be defined as <code>noexcept</code>) may also apply in the case of value constraints development. We consider it an open issue.</p>
<h2>Disabling run-time checks</h2>
<p>Unlike with the static analysis approach, evaluating value constraints adds run-time overhead. Wile the overhead is acceptable in some cases, it is desirable to be able to globally disable the checks in other cases. This issue is similar to C-style <code>assert</code>s, which can be retained in debug/test builds but removed in release builds. C-style <code>assert</code>s are disabled by recompiling the entire program; this includes all 3rd party libraries, or linking with the alternative pre-compiled versions. Can this be made better for language-level value constraints? <a href="N1800">[N1800]</a> suggests an implementation (for preconditions) that could be capable of handling such requirement: each function has two entry points: first that checks the precondition and then evaluates the function, second that skips the evaluation of the precondition. Once you have the two entry points it is just the question of changing the addresses. This solution results in bigger libraries although the final executables could be optimized.</p>
<h1>Assisting static analysis</h1>
<p>Automated tools already perform static analysis, even without any support from the programmer. However, additional hints from developers could enable even further analysis, or enable vendors to add analysis in compilers at lower expense. In the example like the following, a compiler can fairly easily detect that a potential undefined behaviour is at hand:</p>
<pre>int* produce()
{
if (cond) return &global;
else return nullptr;
}
void consume(int* p)
{
use(*p);
}
consume(produce());
</pre>
<p>But even here, certain problems occur. What if the two functions are compiled separately; e.g., if <code>produce</code> is part of a separate third party library? Even if compiler performs a per-file analysis, it may not have sufficient resources (RAM) to perform a global link-time analysis. Even if the analysis is successful and detects a potential undefined behaviour, it doesn't tell us who of the three: author of <code>produce</code>, author of <code>consume</code> or the guy who assembles them, is responsible for the situation and should fix the problem. This is somewhat similar to the situation we face today with template instantiation error messages. Compiler sees that there is a syntax/type error, it can give you the entire context, but it cannot tell at which level of instantiation process the source of the problem lays.</p>
<p>Also, as shown in the example with <code>sqrt</code> it is sometimes not possible to tell from only observing the reads from a variable what the function's requirement is. In the case of <code>sqrt</code> it is not the undefined behaviour that we want to avoid but an infinite recursion.</p>
<p>Another reason where assisting the static analysis may prove useful is when there is more than one way to express a given condition. Consider the following code:</p>
<pre>
class Vector
{
const T& front() const; <em>// requires: !this->empty()</em>
<em>// ...</em>
};
void test(Vector & vec)
{
if (vec.size() != 0)
use(vec.front());
}
</pre>
<p>You know that <code>vec.size() != 0</code> and <code>!vec.empty()</code> mean the same thing, but compiler may not, especially if it cannot look inside the definitions of member functions (because they are compiled separately).</p>
<p>However, an analysis like this can produce too many false warnings. This calls for another [[attribute]] for indicating that the programmer doesn't want certain parts of the code to be warned about potential value constraint violations.</p>
<h2>How long does a condition hold?</h2>
<p>We illustrate the issue in question with the following two examples.</p>
<pre>
Iter test(Iter b, Iter e, Value_type<Iter> v)
{
std::sort(b, e);
fun();
std::binary_search(b, e, v); // requires: is_sorted(b, e)
}
</pre>
<p>Assuming that a static analyser can somehow figure out that <code>sort</code> leaves elements in the state that satisfies the condition <code>is_sorted</code>, can it be sure that the condition still holds when <code>fun</code> is finished? After all <code>fun</code> could be manipulating iterators that alias <code>b</code> and <code>e</code>. Apparently, static analysis cannot give us a 100% bug-free guarantee. It can only helps detect certain bugs. This is where run-time checks can still prove useful even after a heavy static analysis.</p>
<p>Second, it is obvious that a certain condition does not last forever. How is the analyser supposed to know when a given condition ceases to hold? One easy answer would be to say that when a non-<code>const</code> operation is called on the object all conditions it might have satisfied are now considered not satisfied. But this would break even simple use cases:</p>
<pre>void test(std::vector<int> & vec)
auto b = vec.begin(); <em>// non-const: invalidates all conditions</em>
auto e = vec.end(); <em>// non-const: invalidates all conditions</em>
std::sort(b, e); <em>// requires: valid_range(b, e)</em>
</pre>
<p>Even if the analyser knows that <code>vec.begin()</code> and <code>vec.end()</code> form a valid range, they are a non-<code>const</code> operations and invalidate any assumptions about their value/state. Any language feature for assisting static analysis must provide a way of specifying which operations invalidate which conditions (e.g., a way of declaring some functions as non-modifying even when they are non-<code>const</code>). But this is likely to make the specifications very complicated, and discourage everybody from using the feature.</p>
<h1>"Properties": a hypothetical language feature</h1>
<p>In this section we describe a language feature that would enable defining value constraints in a somewhat different way than the "imperative" approach described in <a href="#N1962">[N1962]</a>. We call it <em>properties</em>, which have been described in <a href="#N3351">[N3351]</a>. A property is a new kind of "entity" in the language: it is neither an object, nor a function, it is just something else. It is introduced by an invented keyword "<code>property</code>":</p>
<pre>template <typename T>
property bool is_non_empty (std::vector<T>);
</pre>
<p>A property is something that an object, or a group of objects can acquire at a certain point in time, and then loose at a different point in time. There is no function-body associated with the property: it only has a name. A property can be used in specifying pre- and postconditions:</p>
<pre>
template <typename T>
class vector
{
void push_back (T const&); // post: is_non_empty(*this);
const T& back() const; // pre: is_non_empty(*this);
};
vector<int> v; // doesn't have property is_non_empty yet.
v.push_back(1); // acquires property is_non_empty
int i = back(); // required property is present
v.pop_back(); // looses property is_non_empty
</pre>
<p>How do we know when a property is lost? In the most simple case we could say that every mutating (non-const) function called upon our object discards all its properties. In our example, we know that property <code>is_non_empty</code> is not always lost after the call to <code>pop_back</code>, but in order to keep the specification language fairly simple we may need to accept this simplification. But the rule "discard every property on non-const function call" would imply that in our case even calling <code>back()</code> discards the property, so a more complex way of specifying how the properties are preserved may be required.</p>
<p>So, what do we buy using properties rather than considering any boolean expression such a property? First, properties are pure: they have no side effects. Second, we can express value constraints that are not expressible with expressions:</p>
<pre>
template <typename Iter>
property bool valid_range(Iter begin, Iter end);
template <typename T>
class vector
{
// invariant: valid_range(this->begin(), this->end());
};
template <typename Iter>
void sort(Iter begin, Iter end) // pre: valid_range(this->begin(), this->end());
</pre>
<p>In this model of static analysis, one function's preconditions are matched with other function's postconditions. But because properties have no body, it is not possible for the static analyser to determine if a function that declares a property in its postcondition really satisfies it. Properties can be mixed with normal boolean predicates, though. The author decides if his value constraint is implementable or not.</p>
<p>We do not propose to add such properties to the language. We just want to show a different perspective on value constraints. <a href="#N1962">[N1962]</a> also offers this perspective, but we fear that the focus on broken contract handlers and the order of evaluation of different value constraints, might have obfuscated this idea. A similar effect (as having properties) could be achieved by annotating some value constraints (which use normal expressions) that they must never be evaluated. </p>
<h1>Interactions with other C++ features</h1>
<h2>When should precondition hold?</h2>
<p>A common answer to this question is "after function parameters have been initialized, before its first instruction is executed." While it looks good in typical simple examples, consider the following case:</p>
<pre>void fun(Tool * const tool, int const i)
// requires: tool != nullptr
// requires: tool->value() >= 0;
{
line_1: int j = transform(i);
line_2: int k = process(tool->value());
}
</pre>
<p>A precondition constrains the state of a remote object of type <code>Tool</code>, its state can change asynchronously. Suppose we can evaluate the precondition upon entering the function. We determine that it is satisfied. We successfully execute instruction <code>line_1</code>, we will now proceed to instruction <code>line_2</code>. It is only now that we really need the precondition to hold, but by now the state of the remote object referred to by pointer <code>tool</code> might have already changed (perhaps function <code>transform</code> modified it)</code>. While the precondition held upon entry, the same condition caused an undefined behaviour later on. Even if one argues that function must not break the precondition itself, one should still consider the possibility that while executing <code>line_1</code> another thread may concurrently update the object referred to by <code>tool</code>. So, should precondition hold for the entire duration of its function? Or is it a bad idea to express a constrain on remote objects that we do not obtain by value? We do not have a ready answer for this question, but the question is very important, because this kind of interface is used in STL algorithms: they obtain and return iterators, which are handles to remote parts likely aliased and accessible by other threads.</p>
<h2><code>constexpr</code> functions and literal types</h2>
<p><code>constexpr</code> functions can be evaluated at run-time or at compile-time. Ideally, a compile-time evaluation of such function should result in compile-time error when its precondition or postcondition is broken. This is possible if expressions in preconditions and postconditions are core constant expressions. It appears reasonable to require that <code>constexpr</code> functions have only <code>constexpr</code> value constraints.</p>
<p>A similar question needs to be answered for literal types and invariants. For literal types it is required that they have at least one non-copy/move <code>constexpr</code> constructor. This constructor can be used to create a compile-time constant, whose invariant is expected to hold. This may require that the invariant should also be <code>constexpr</code>, as otherwise it is impossible to verify it at compile time. On the other hand, the interface of user-defined literal types can be divided into compile-time (<code>constexpr</code>) and run-time part. The effects of the other one may alter other parts of the program state that may only be invariant-verified with run-time expressions. More, some constructors are <code>constexpr</code> even for non-literal classes: their purpose is to guarantee the static initialization of global objects. It is not clear if this should affect the <code>constexpr</code> requirement on the class invariant.</p>
<h2>Function's public interface</h2>
<p>For the purpose of specifying the semantics of value constrains, we may need to redefine the concept of class's public interface. Consider the following definition:</p>
<pre>class Account
{
public:
void modify(Param p);
friend void swap(Account& a1, Account& a2);
private:
// ...
};
</pre>
<p>Function <code>swap</code>, although it is not a public member function, clearly is part of <code>Account</code>'s public interface. I.e., we allow that it temporarily breaks the invariant of objects <code>a1</code> and <code>a2</code>. The technique with defining operator-like free functions as friends is not just a trick. In fact it is sometimes recommended for operators like <code>operator==</code> when the two arguments are to be treated symmetrically.</p>
<p>At this point we are not sure if it is sufficient to define class's public interface as the set of its public member functions and its friend functions. An additional way of specifying what is class's public interface may be necessary. This is a problem not limited to value constraints. Such specification could be useful for enabling a more fine-grained function lookup rule. Current ADL is known to pick too many overloads.</p>
<h2>When should a class invariant hold?</h2>
<p>When is class invariant supposed to hold? Objects are manipulated via class's <em>public interface</em>. Functions from class's public interface (public functions or friend functions) often need to compromise the invariant, but they always put the invariant back when they finish -- even via an exception. This means that as long as no function from the object's public interface is being invoked on it, or any of its subobjects manipulated, the object's invariant should hold. Consider:</p>
<pre>Tool t;
_1:;
fun1()
_2:;
fun2();
_3:;
t.fun();
_4:;</pre>
<p>In run-time checking approach it is verified that the invariant of <code>t</code> holds at points <code>_1</code>, <code>_3</code> and <code>_4</code>. But we also claim that the invariant should hold at point <code>_2</code>. It is impractical to inject a run-time check in there, but is static analyser detects that the invariant may be broken at <code>_2</code>, it should definitely report it as invariant breach.</p>
<p>This is different from the common notion that invariants should hold before entering any public function or destructor and after leaving any public member function or constructor. For instance, inside a public function you can invoke other public functions and around these nested calls you do not expect the invariant to hold. And conversely, an invariant should hold at <em>any</em> time between the calls to public interface. Putting the run-time checks in thus identified places is impossible, which proves that the approach "check before and after the call to any public member functions" are the consequence of implementation limitations -- not the definition of a class invariant. This also shows that run-time checks are not enough to guarantee the safety of the program: static analysis may be required to complement them.</p>
<h2>Composing invariants</h2>
<p>Given some class <code>D</code>, apart from its "direct" invariant, we expect that invariants of <code>D</code>'s bases classes and <code>D</code>'s data members also hold. This can be implicit, you do not have to make recursive definitions yourself, similarly like you do not have to specify in the destructor which subobject's destructors need to be called. But this does not cover all cases. Consider class <code>optional</code> (similar to Boost.Optional), it can be implemented as follows:
<pre>
template <typename T>
class optional
{
bool is_initiailzed_ = false;
std::aligned_storage_t<sizeof(t), alignof(T)> storage_;
T* storage() { return *static_cast<T*>(&storage_); }
public:
explicit operator bool() const { return is_initialized_; }
T& operator*() {
assert (is_initiailzed_);
return *storage();
}
optional(const T& v) {
new (storage()) T(v);
is_initiailzed_ = true;
}
~optional() {
if (is_initiailzed_)
storage()->T::~T();
}
};
</pre>
<p>
Obviously, we store (sometimes) an object of type <code>T</code> inside, but it is neither a base class nor a member sub-object. Yet, if it is there (if optional object contains a value), we want its invariant to hold, and compiler may not be able to deduce it. We might need to express a "conditional" invariant:</p>
<pre>// invariant: !is_initialized_ || invariant(*storage());</pre>
<p>Similarly, a vector of <code>T</code>s (<code>std::vector<T></code>) can be thought of as being composed of the <code>T</code>s it contains. This is reflected in how its equality comparison is defined and how const-ness is propagated. A value of the container is composed of the values of its elements. In a similar manner, we would like to be able to express invariants on composed types, i.e., the vector's invariant holds iff some vector-specific conditions are satisfied and all vector elements' invariants hold. We are not quite sure, if this needs to be specified explicitly, or is it not enough for the machine to observe that if there is some nested T accessible from the vector, its invariant must hold. But will the machine know that the result of <code>vec.back()</code> should have its invariant hold? after all, calling <code>back()</code> is not always allowed, and may render a undefined behaviour.</p>
<p>This issue does not appear if we adopted the view that invariants hold immediately before and after the call to public interface functions. But we do not constrain our analysis to this "run-time checks" view.</p>
<p>This also implies that when two threads run concurrently and one is in the middle of modifying object <code>x</code>, the other thread should not be able to see the partial state of <code>x</code> in which the invariant does not hold.</p>
<p>Another open question is if we should check invariants of member subobjects if they are references (and therefore do not pertain to the master object’s value).</p>
<h2>Protected members</h2>
<p>Can protected member functions be called in pre- and post-conditions? In public functions, this makes no sense: the user of the class may not have access to protected functions; and it is expected that the user in order to verify if a precondition holds should be able to evaluate the condition herself.</p>
<p>On the other hand, protected functions may also need to specify their preconditions as they constitute an interface for deriving classes (which can also be considered users), and for them calling other protected members appears reasonable.</p>
<p>Similarly, it is possible that class's protected interface may assume an invariant that is narrower than the class's public interface's invariant. Protected members may require less of the program state than the public members, but they still may require something. In other words, we claim that a class exposes two interfaces: one for external callers and the other for derived classes; the two interfaces may require two sets of value constraints. Not sure if this use case is worth complicating the language.</p>
<h1>Constraining STL</h1>
<p>As a usefulness test, any proposed value constraint framework should be checked if it is able to express value constraints in STL. We consider some selected examples. We do not insist that a proposed framework should be able to handle them, but consider it rather a test of expressive power. The goal is to help determine where we want to stop in expressing the semantics in the language.</p>
<h2>Case 1: a valid range</h2>
<p>This is probably the most difficult one to handle. Nearly any algorithm on STL ranges requires that <code>end</code> is reachable from <code>begin</code>. It cannot be validated by executing any expression. This is why it is required as a precondition: the caller may have better means of ensuring that this requirement is satisfied. For instance, it is obvious that <code>c.begin()</code> and <code>c.end()</code> called on any STL container form a valid range. Is a value constraints framework capable of expressing that the values of <code>c.begin()</code> and <code>c.end()</code> satisfy the requirements of, say, <code>std::for_each</code>?</p>
<h2>Case 2: sub-ranges</h2>
Similarly, in the call <code>m = std::find_if(b, e, p)</code>, assuming that <code>b</code> and <code>e</code> form a valid range, can it be verified or even expressed that <code>b</code> and <code>m</code> as well as <code>m</code> and <code>e</code> form valid ranges and that these combinations should satisfy the requirement of subsequent STL algorithms about valid ranges?
<h2>Case 3: sorting</h2>
<p>Consider functions <code>sort</code> and <code>binary_search</code> from the Standard Library (we consider only the overloads with the predicate). The former guarantees that it leaves the range sorted with respect to the given predicate. The later requires that the range is <em>partitioned</em> with respect to the given predicate and the given element. Being partitioned is something less than being sorted. for instance range {3, 1, 2, 5, 9, 8, 7} is partitioned with respect to element 5 and <code>operator<</code> but is not sorted.<p>
<h2>Solution with properties and axioms</h2>
Below we show how the above task can be solved with sophisticated features like properties (described above) and axioms (similar to those described in <a href="#N2887">[N2887]</a>).
<h3>Case 1</h3>
<pre>template <typename I>
property bool is_valid_range(I b, I e);
template <typename T>
axiom vec_range(std::vector<T> v)
{
is_valid_range(v.begin(), v.end());
}
template <typename Iter>
void sort(Iter b, Iter e)
precondition{ is_valid_range(b, e); };
vector<int> v = {/*...*/};
sort(v.begin(), v.end());
</pre>
<h3>Case 2</h3>
<pre>template<typename I, typename V>
I find(I b, I e, V v)
precondition{ is_valid_range(b, e); }
postcondition(f) {
is_valid_range(b, f);
is_valid_range(f, e);
// ... more
};
vector<int> v = {/*...*/};
auto i = find(v.begin(), v.end(), 7); // axiom vec_range
auto j = find(i, v.end(), 7); // postcondition of find
</pre>
<h3>Case 3</h3>
<pre>template <typename It, typename T, typename Comp>
bool is_partitioned_for_element(It b, It e, T v, Comp c)
{
return is_partitioned(b, e, [&v](auto&& e) {return cmp(e, v);})
&& is_partitioned(b, e, [&v](auto&& e) {return !cmp(v, e);})
&& all_of(b, e, [&v](auto&& e) {return !cmp(e, v) || !cmp(v, e);});
}
template <typename It, typename T, typename Comp>
axiom sorted_is_partitioned(It b, It e, T v, Comp cmp)
{
is_sorted(b, e, p) => is_partitioned_for_element(b, e, v, cmp);
}
template <typename Iter, typename Comp>
void sort(Iter b, Iter e, Comp cmp)
postcondition{ is_sorted(b, e, cmp) };
template <typename It, typename T, typename Comp>
bool binary_search(It b, It e, T v, Comp cmp)
precondition{ is_partitioned_for_element(b, e, v, cmp) };
</pre>
<p>Can the above tasks be accomplished with "run-time checks" approach? The biggest problem is that <code>is_valid_range</code> is not implementable in the general case as a function (template). The only way to check if two iterators form a valid range is to increment the first one and check if we reach the second one. But in case we get an invalid range, such function rather than returning <code>false</code> will run forever or render an undefined behaviour. Rather than introducing a new notion of a "property", we could annotate (with attributes) some functions as "not defined on purpose". If the compiler sees such function in a value constraint it skips the run-time check (but may still perform static analysis). This way we could mix normal functions with non-implementable functions in preconditions.</p>
<p>Again, we do not propose to standardize the above, but we show that preconditions in STL algorithms are expressible with a sufficiently complex facility.</p>
<h1>What do we need to standardize?</h1>
<p>The language feature of value constraints can be divided into two main parts. (1) What value constraints we define and how, (2) how do we handle run-time response to a broken value constraint.</p>
<h2>Defining value constraints</h2>
<p>At this point it is too early to decide on the details, but one thing appears fairly uncontroversial. Value constraints support needs to accommodate two fairly opposite requirements: (1) no run-time overhead in cases like (<code>operator[]</code> for vectors), (2) guaranteed (in certain situations) evaluation of the predicates (where performance requirement is not critical).</p>
<p>This calls for the following semantics:</p>
<ol>
<li>If a <em>piece of code</em> (a function or a block) <em>relies</em> on a given value constraint <em>C</em> (e.g., a function relies on its precondition, a public member function relies on class invariant), and this code is executed but value constraint <em>C</em> would return false <em>if it were evaluated</em> (but no evaluation is required), the behaviour of the program is undefined. — this accommodates the situations ranging from buffer overflow to calling terminate handlers.</li>
<li>If the control reaches the point where a value constraint <em>could be evaluated</em> (for preconditions this moment is just before function call, etc.), it is <em>unspecified</em> whether the value constraint is evaluated once or not evaluated at all. — this handles the behaviours ranging from performing all run-time checks to disabling them all by a compiler switch or some [[attributes]].</li>
</ol>
<p>One thing that appears non-controversial is that declarations of preconditions and postconditions need to be part of function declaration, so that they are accessible by the function users who may not have access to function definitions. We leave it open whether a value constraint declaration should affect function's signature or type or affect the overload resolution mechanism; although it looks like affecting function's type would make it impossible to retrofit value constraints into the existing code.</p>
<h2>Run-time response</h2>
<p>One option is not to standardize what should happen when we detect at run-time a broken value constraint (whether to throw or terminate or abort or ignore), and let the vendors decide how they want to handle these cases. With this approach a minimum conforming implementation only needs to syntax- and type-check the declarations.</p>
<p>But there may be parts of programs that require a guaranteed run-time evaluation of a precondition in order to prevent the subsequent function execution and a guaranteed release of critical resources. The minimum requirement then is to annotate "critical" value constraints and a call to <code>std::terminate</code>, whose goal is already to collect the critical resources whose release cannot be skipped.</p>
<p>It may be useful to standardize a set of [[attributes]] for giving hints on what conditions to evaluate value constraints, e.g., "evaluate only if <code>T</code> satisfies some requirements", or "this constraint has complexity O(N), evaluate it only when O(N) and bigger complexities are enabled", "never evaluate this precondition", or "never evaluate this function if it is in a value constraint".</p>
<h1>Acknowledgements</h1>
<p>Lots of content in this paper is inspired by work in <a href="#N1962">[N1962]</a>, <a href="#N2887">[N2887]</a> and <a href="#N3351">[N3351]</a>.</p>
<p>Lawrence Crowl reviewed the paper, highlighted issues and suggested improvements.</p>
<p>Gabriel Dos Reis suggested the "STL test" for a precondition framework.</p>
<p>Joël Lamotte offered a number of useful suggestions that improved the quality of the paper.</p>
<h1>References</h1>
<ul>
<li><a name="ACSL">[ACSL]</a> Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prevosto, "ACSL: ANSI/ISO C Specification Language" (<a href="http://frama-c.com/download/acsl_1.4.pdf">http://frama-c.com/download/acsl_1.4.pdf</a>),</li>
<li><a name="N1800">[N1800]</a> Lawrence Crowl, Thorsten Ottosen, "Contract Programming For C++0x" (<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2005/n1800.pdf">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2005/n1800.pdf</a>),</li>
<li><a name="N1962">[N1962]</a> Lawrence Crowl, Thorsten Ottosen, "Proposal to add Contract Programming to C++ (revision 4)" (<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html</a>),</li>
<li><a name="N2887">[N2887]</a> Gabriel Dos Reis, Bjarne Stroustrup, Alisdair Meredith, "Axioms: Semantics Aspects of C++ Concepts" (<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2887.pdf">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2887.pdf</a>),</li>
<li><a name="N3248">[N3248] Alisdair Meredith, John Lakos, "<code>noexcept</code> Prevents Library Validation" (<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2011/n3248.pdf">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2011/n3248.pdf</a>)</li>
<li><a name="N3351">[N3351]</a> Bjarne Stroustrup, Andrew Sutton et al., "A Concept Design for the STL" (<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2012/n3351.pdf">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2012/n3351.pdf</a>),</li>
<li><a name="N4075">[N4075]</a> John Lakos, Alexei Zakharov, Alexander Beels, "Centralized Defensive-Programming Support for Narrow Contracts (Revision 6)" (<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4075.pdf">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4075.pdf</a>),</li>
<li><a name="N4110">[N4110]</a> J. Daniel Garcia, "Exploring the design space of contract specifications for C++" (<a href="http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4110.pdf">http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4110.pdf</a>),</li>
<li><a name="SPECS">[SPECS]</a> K. Rustan M. Leino, Peter Müller, "Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs" (<a href="http://www.codeplex.com/Download?ProjectName=specsharp&DownloadId=84056">http://www.codeplex.com/Download?ProjectName=specsharp&DownloadId=84056</a>).</li>
</ul>
</body>
</html>