220 11644 article Path: news.gmane.org!not-for-mail From: =?UTF-8?Q?Andrzej_Krzemie=C5=84ski?= Newsgroups: gmane.comp.lang.c++.isocpp.proposals Subject: Value constraints (or contract programming in C++) Date: Fri, 4 Jul 2014 07:52:03 -0700 (PDT) Lines: 1084 Approved: news@gmane.org Message-ID: Reply-To: std-proposals@isocpp.org NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_80_32937670.1404485523485" X-Trace: ger.gmane.org 1404485534 16982 80.91.229.3 (4 Jul 2014 14:52:14 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 4 Jul 2014 14:52:14 +0000 (UTC) To: std-proposals@isocpp.org Original-X-From: std-proposals+bncBDT2DGOJ34DBBFH73KOQKGQEVR2STWI@isocpp.org Fri Jul 04 16:52:06 2014 Return-path: Envelope-to: gclcip-std-proposals@m.gmane.org Original-Received: from mail-vc0-f198.google.com ([209.85.220.198]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1X34qL-0004oq-Sx for gclcip-std-proposals@m.gmane.org; Fri, 04 Jul 2014 16:52:06 +0200 Original-Received: by mail-vc0-f198.google.com with SMTP id hy10sf5125526vcb.9 for ; Fri, 04 Jul 2014 07:52:04 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=date:from:to:message-id:subject:mime-version:x-original-sender :reply-to:precedence:mailing-list:list-id:list-post:list-help :list-archive:list-subscribe:list-unsubscribe:content-type; bh=9RyGYOTsQvnMCKmJ0l5YI6dXT59rCO9FWL0nQnt/Yrk=; b=vmIIcGtUSF48aXr7xa1yvIGh20B+eaMBU8lfpokkS/3mokyiG1Q5p8B9WjbxHvPI0q +5WPQS8oZsVnHnN5SAgxuBi8UEWBXro2ElNQbLeMf0i8GXi+x/GUitwbEfMqnfEtZl/q y9sfeH/6fyhL+v8I+idW1qbtcdoTmoCEaKGMh7lBMaCm1GivtwxHNNTVvYL8T4kcvft8 gi5XoxKZob4sSfR7vN4VVW8/ZZe+6WEzRnZa76FR6eIR08+iXeomeyLTdoIPkxTRy2/p Fakuy0w5gXMsC3jesQygEVqW5XLqnvkHAeqSDUjNVVd7DRu4rxM8C32UOhoeXLneZR0Y ib7A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:date:from:to:message-id:subject:mime-version :x-original-sender:reply-to:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe :content-type; bh=9RyGYOTsQvnMCKmJ0l5YI6dXT59rCO9FWL0nQnt/Yrk=; b=V66FhyMicbeY4bEIiCkSq+9fXhooMRnWgyO2mCHtvkmht+Ht7d7lXSlCCJVLw4uun7 /+Vq/dATfqD84roJwb2Edaut3PH79pk9hCAqqwyfrBpju5vn3StwfqrP323Dx+/jCq76 Y+AYtNa1T7bkYntam4EJNSnxMDoU03neS+qTamAp8NDu8QZTuYb4VlL5g2Fuo+VoJf6L Q9CaKJgCggd19KAllo6/ZclnX+WzSkGIK5j31aVJ/i5oT4I7K8RYsQSKnxIdsCSPa4uW 4YG4hut2joGPgr+1LP/qchwi6qZ0c7Te1+Rwe8MrdXAW4LhjWx09kl23exFJeaMQNgvU wCKA== X-Gm-Message-State: ALoCoQkz50Nhqs6ruGJJ9Yy0UL32u7Zf49q0fVCdcoFdJFgiaGrSQ+pS2LpDqFvuqCVUzeSDxZWq X-Received: by 10.58.83.133 with SMTP id q5mr5771088vey.31.1404485524883; Fri, 04 Jul 2014 07:52:04 -0700 (PDT) X-BeenThere: std-proposals@isocpp.org Original-Received: by 10.140.17.19 with SMTP id 19ls902738qgc.69.gmail; Fri, 04 Jul 2014 07:52:04 -0700 (PDT) X-Received: by 10.140.107.35 with SMTP id g32mr199266qgf.2.1404485524018; Fri, 04 Jul 2014 07:52:04 -0700 (PDT) X-Original-Sender: akrzemi1@gmail.com Precedence: list Mailing-list: list std-proposals@isocpp.org; contact std-proposals+owners@isocpp.org List-ID: X-Google-Group-Id: 399137483710 List-Post: , List-Help: , List-Archive: List-Subscribe: , List-Unsubscribe: , Xref: news.gmane.org gmane.comp.lang.c++.isocpp.proposals:11644 Archived-At: ------=_Part_80_32937670.1404485523485 Content-Type: multipart/alternative; boundary="----=_Part_81_2415517.1404485523486" ------=_Part_81_2415517.1404485523486 Content-Type: text/plain; charset=UTF-8 Hi, I wanted to share here my reflections about how C++ could support contract programming (things like preconditions). One alternative to the "traditional" design-by-contract is considered. I share the html document on GitHub, so there is an inconvenience involved: you have to see it in raw form, download and then reopen in the browser. Here's the link: https://github.com/akrzemi1/contract/blob/master/contract.html I also enclose it for convenience. I would be grateful for any comments. Regards, &rzej -- --- You received this message because you are subscribed to the Google Groups "ISO C++ Standard - Future Proposals" group. To unsubscribe from this group and stop receiving emails from it, send an email to std-proposals+unsubscribe@isocpp.org. To post to this group, send email to std-proposals@isocpp.org. Visit this group at http://groups.google.com/a/isocpp.org/group/std-proposals/. ------=_Part_81_2415517.1404485523486 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hi,
I wanted to share here my reflections about how C++= could support contract programming (things like preconditions). One altern= ative to the "traditional" design-by-contract is considered.

I shar= e the html document on GitHub, so there is an inconvenience involved: you h= ave to see it in raw form, download and then reopen in the browser. Here's = the link:

https://github.com/akrzemi1/contract/blob/master/contract.= html

I also enclose it for convenience. I would be grateful for any = comments.

Regards,
&rzej

--

---
You received this message because you are subscribed to the Google Groups &= quot;ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to std-proposa= ls+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
Visit this group at http://groups.google.com/a/isocpp.org/group/std-proposals/<= /a>.
------=_Part_81_2415517.1404485523486-- ------=_Part_80_32937670.1404485523485 Content-Type: text/html; charset=UTF-8; name=contract.html Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename=contract.html X-Attachment-Id: 464541be-b443-41f5-89bd-e95ead9383bf Content-ID: <464541be-b443-41f5-89bd-e95ead9383bf> Value constraints

Author: Andrzej Krzemieński

Value constraints

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 sem= antics" to stress that we do not necessarily want to copy solutions that ot= her imperative programming languages adapt. we want to change a focus from = how broken contracts are responded to in run-time, to how contract violatio= ns can be detected at compile-time. This is a high-level overview of the pr= oblem, and we are not even covering the things like sub-contracting or othe= r interactions with OO features.

What do we need?

The 'features' we describe here can be collectively called value constr= aints. We want to use them to express in the language that certain combinations of= values of certain objects=20 at certain times are invalid and are intended (and expected) never to occur= ..

Specify function's domain

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 over real numbers is not defined for negative numbers.=20 What does it mean for a function in a programming language like C++=20 that it is not defined? Currently there are two approaches. One is to detec= t=20 the value of the parameter(s) that the function should not be prepared for= =20 and execute a different logic: returning a special value, throwing an excep= tion, etc.=20 Using our example with a square root, a corresponding function sqrt()= could be defined as follows:

double sqrt(double x)
{
  if (x >=3D 0.0) {
    // do proper algorithm
  }
  else {
    return numeric_limits<double>::signaling_NaN();
    // or throw an exception
  }
}

What it effectively does is to change the function's domain. Now the fun= ctions 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".=20 This has an unintended consequence: our function can be used for detecting = negative numbers: 

double is_negative(double x)
{
  return isnan(sqrt(x));
}

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 assumpt= ion that the undesired values are never passed to the function:

double sqrt(double x)
// requires: x >=3D 0.0
{
  // proper algorithm:
  double y =3D 1.0;
  double prev_y;
=20
  do {
    prev_y =3D y;
    y =3D (y + x / y) * 0.5;
  }
  while (!closeEnough(y, prev_y));
=20
  return y;
}

This uses Newton's Iteration algorithm. The loop will terminate when val= ues y and prev_y become close enough. They will o= nly do that when x is non-negative. Supplying a negative value= will make the loop run forever and hang the program. Even a clever analyse= r is unlikely to detect from the function body that passing a negative inpu= t to this function is something wrong. But everything is fine as long as no= negative number is passed in. 'Announcing' that the function is not prepar= ed 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 ob= vious. This risks an unintended negative program behaviour, like a halt, or= a UB. However, it is often preferred because of performance and inability = to come up with a reasonable fall-back action. Consider std::vector::= operator[], it does not check the bounds for performance reasons. If= it was used in the following code:

for (int i =3D 0; i !=3D vec.size(); ++i) {
  if (i > 0) cout << ", ";
  cout << vec[i];
}

The condition in the loop already checks if the index is within bounds. = If operator[] was also checking the same condition inside, we = would be wasting time on doing redundant checks. Also, for some functions i= t is not possible to think of any fall-back action. For instance std:= :vector::swap must not throw exceptions and returns void, yet, it is not well defined when two vectors' allocators do not compare = equal.

Not checking for argument being within domain and delegating the check t= o the callers is desirable, especially that the caller is in a better posit= ion in verifying if the domain of the function. Consider:

return sqrt(abs(x));

The caller can be sure that no negative value is passed to function sqrt() even though no check is performed at all. Function domain d= efined this way is a contract 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 value= s 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 respo= nsible 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>

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 too= ls. How the tools can handle this is a secondary issue, but the behaviour c= an be: (1) automated documentation generation, (2) additional warnings from= static analysers, (3) additional instrumentation injected by compilers, (4= ) compiler optimizations based on domain declarations.

Specify function's co-domain

In the above example with function abs() a hypothetical too= l could detect that expression sqrt(abs(x)) is always fine onl= y if it knew that the co-domain of abs is equal (or smaller) t= han the domain of sqrt. We need to be able to constrain the al= lowed function output in order for automated tools to be able to verify if = other functions' domain requirements are satisfied.

In this case a function author specifies the contract and (likely) the s= ame 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 perso= n that declares and later ensures the obligation. And conversely, if the au= thor makes an error in the function, he is equally likely to make an error = in specifying the contract.

Block-level assertions

This type of value constraint is quite familiar to many C++ user, as it = is implemented with macro assert and some similar tools in man= y libraries. If we think of it as a contract, this time a function author d= efines it, he ensures that it holds, and he is the benefactor of the contra= ct: he guarantees something to himself, namely that certain state of a bloc= k-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 h= e can be held accountable for, and relies on the guarantee expressed with t= he assertion.

Class-level assertions

A similar constraint on variables is often required for (non-static) dat= a members of objects of a given class. Consider the following example:

class WeighedAverage
{
  double wgt1_ =3D 0.5;
  double wgt2_ =3D 0.5;
public:
  double average(double val1, double val2) const;=20
  // ensures: answer is between val1 and val2
  { return wgt1_ * val1 + wgt2_ * val2; }

  void set_1st_weight(double w1);=20
  // requires: w1 between 0.0 and 1.0
  { wgt1_ =3D w1; wgt2_ =3D 1.0 - w1; }

  // always true: wgt1_ between 0.0 and 1.0
  // always true: wgt2_ between 0.0 and 1.0
  // always true: wgt1_ + wgt2_ =3D=3D 1.0
};

Note the three comments at the bottom. They are something that could be = expressed with macro assert, except that assert i= s an expression and cannot be put at the class scope. Note also that member= s wgt1_ and wgt2_ are private. So, we are not dec= laring 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 r= eturn). 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.

Class-level assertions (or class invariants) could be use 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.

Specify equivalent expressions

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 b= e checked in two ways: cont.empty() and cont.size() !=3D= 0. The latter is more general and could be used to check for emptin= ess, but there are occasions where the former can perform faster. This just= ifies the existence of the two forms. However, the job of matching one func= tion's domain with other function's co-domain would be severely impeded if = either specified the contract with a different (albeit equivalent) expressi= on. consider:

template <typename T>
class vector
{
  void resize (size_t s); // ensures: this->size() =3D=3D s
  const T& front() const; // requires: !this->empty()
};

vec.resize(1);
return vec.front();       // safe?

Can we match what resize guarantees with what front expects? The two expressions are different. It would be much easier i= f we were able to explicitly declare that for any container expressions cont.empty() and cont.size() !=3D 0 are equivalent. = This is somewhat similar to class-level assertions, but the declaration app= lies to more than one class, now we are only interested in the public inter= faces, and we can express equivalence between expressions that have side ef= fects. for instance, we can specify that cont.clear() is equiv= alent to cont.resize(0). Out of all "constraints" described in= this section, this is the only one where term "value constraint" is inadeq= uate. This is a constraint on the semantics of expressions.

Loop variants

This is somewhat similar to an assertion. It can help convince oneself t= hat a non-trivial loop will ultimately terminate. Sometimes it is not easil= y seen, because there is no loop counter. We may for instance inspect eleme= nts in the collection by skipping some elements, increasing or shrinking, t= he collection. A loop variant is an expression that evaluates to an integra= l non-negative number. It is expected that in each loop iteration evaluatin= g 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>

A framework for supporting value constraints need not address all the ab= ove needs. We believe that only supporting the declaration of function doma= in is a big help in itself. Note that while assertions loop variants need t= o 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.

What use can be made of value constraints?

Value constraints exist, even though there is no language support for th= em in the language. We have seen in the above examples that comments were u= sed to convey the information. In this section we list the benefits obtaine= d form standardizing or formalizing value constraints this way or the other= ..

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 s= ource code comments. For instance [ACSL] uses the fol= lowing notation: 

/*@ requires x >=3D 0;
    ensures \result >=3D 0;=20
*/
double sqrt(double x);

But for structured comments like the above, C++ has an alternative: [[at= tributes]]. Attributes are akin to comments because they cannot affect the = semantics of the program. On the other hand they can be used as hints for o= ptimizations, warnings and any kind of program analysis. If the expectation= of value constraints is to affect the program behaviour, attributes will n= ot do, and a special language feature would need to be devised.

=20

An ideal — and unrealistic — support for value constraints i= s for compiler to check any possible flow in the program and signal a compi= ler error whenever a breach of the constraint is going to happen. Because t= his is not doable, the we aim at the support that is not entirely satisfact= ory, but believed to be better than none.

Improved documentation

One of the obvious uses of formalized value constraints is the automated= generation of documentation. Even if developers do not use any tool for ge= nerating documentation, there is still a gain. When a developer sees the de= claration of the function she is going to use, she can immediately see the = value constraints along. If they are a language feature, developers are mor= e encouraged to use them (even though comments would do). Since this does n= ot affect program semantics [[attributes]] are sufficient.

Static analysis

Value constraints could enable static analysers to detect a potential br= each of value constraints and issue warnings. Again, using value constraint= s this way does not affect program semantics, so [[attributes]] would do.

Constraint-based compiler optimizations

In that case, compiler is able to arbitrarily change the behaviour of th= e 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 attrib= utes will not suffice, and we need a language extension for specifying valu= e constraints.

Auto-generation of runtime checks

This is what Eiffel provides and what [N1962] pro= poses. Value constraints need to be C++ expressions. An implementation can = (optionally) inject, at well defined places, a code that evaluates at run-t= ime expressions representing value constraints. If any (boolean) expression= evaluates to false, a certain action (like calling std:= :terminate) 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.

Run-time evaluation of value constraints

In this section we focus on one possible approach: treating value constr= aints as expressions and evaluating them at run-time.

Side effects of the expressions

Using expressions with side effects in value constraints is generally di= scouraged, 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 overhe= ad, and especially the run-time complexity as a side effect. To minimize th= e possibility of invoking a function with a side effect = [N1962] proposes that only const-qualified member function= s are allowed; but even these can modify non-member variables, and it is no= t only member functions that may need to be used to express value constrain= ts. Ideally, we would like to use only pure (referentially transpa= rent) expressions, but C++ as of today does not offer the possibility of de= tecting if an expression is pure. Although the definition of relaxed = constexpr functions makes a step towards pure functions.

A practical question to be answered, given the syntax from [N1962], is if the following to be a legal code for detecting if = run-time value constraint checks are enabled?

int preconditions_on =3D false;
void test() precondition{ preconditions_on =3D true; }
{
  cout << "preconditions are on: " << preconditions_on;
}

And similarly, is the following a reliable way of checking if a number i= s negative?

double sqrt(double x) precondition { x >=3D 0.0; };

double is_negative(double x)
{
  set_precondition_broken_handler(&throw_exception);
  try { sqrt(x) };
  catch (exception const&) { return true; }
  return false;
}

Value constraints in overloaded functions

Consider the following declaration:

template <typename IIT> // requires: InputIterator<IIT>
void displayFirstSecondNext(IIT beg, IIT end);
// requires: std::distance(beg, end) >=3D2

Is function template std::distance referentially transparen= t? The answer is: it is not templates that can or cannot be pure but functi= ons. Some functions instantiated from this template will be pure, others wi= ll not — it depends what iterator type the template will be instantia= ted with. Consider InputIterator. In the worst case (of = std::istream_iterator) incrementing the iterator invalidates other i= terators referring to the same stream. This is a tricky behaviour: by chang= ing our internal copies of objects (iterators), we alter (invalidate) other= , external objects. Function std::distance does increment iter= ators. If our precondition was to be evaluated, this might cause a UB in th= e program.

Thus, we have an expression; it is pure and natural to use for some inst= antiations, and has severe side effects for other instantiations. If we wan= t it to be evaluated only in certain instantiations, another feature needs = to be provided. For instance, we will need to specialize a template only to= be able to specify a different precondition, or add an annotation that thi= s precondition should not be evaluated if certain compile-time predicate ev= aluates to true. clearly, on global switch (similar to N= DEBUG) saying "disable/enable all value constraint evaluations" will= not be enough.

Inadvertent increase in run-time complexity

There are other reasons for having a more fine grained control of which = checks should be enabled. Consider a binary search algorithm. Its runtime c= omplexity is O(log n). It has an obvious precondition that the r= ange we search through is sorted. Performing the sorted check has complexit= y O(n). Thus by evaluating the precondition, we change the algor= ithms complexity. This might be unacceptable, even for some debug/testing b= uilds. 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 pra= ctise a developer adds an obvious precondition, which would be his primary = task, and forgets the secondary task of specifying (using some contract-spe= cific sub-language) the conditions under which this precondition shall be e= valuated.

Run-time response to a broken contract

[N1962] proposes that the action taken upon viola= ting a value constraint should be configurable by the programmer. While we = agree this should be configurable, we object to the way of achieving this b= y std::set_terminate-like registering function. std::set= _terminate can be called multiple times from multiple places: differ= ent, possibly dynamically-loaded/shared libraries. This makes sense for std::terminate. Every part of the system may acquire a critic= al resource: one that has to be released even if "exception handling m= ust be abandoned for less subtle error handling techniques". In that case t= he component also needs to register an additional clean-up function. In cas= e of broken contract situation, we do not need or want that. We believe onl= y the person that assembles the final program from the components and libra= ries, should be empowered to to decide how broken contracts are handled. On= ly 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 th= at: they do not know in what environment they will be used.

Additionally, the std::set_terminate mechanism has a certai= n flow. Unless you apply some syntactic contortions, you cannot set the han= dler for functions executed before main().

We are not aware of any mechanism currently available in C++ that would = facilitate our needs. But since function main 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 main that would indicate what the user's preference = is on the handling of broken contracts.

Assisting static analysis

Automated tools already perform static analysis, even without any suppor= t from the programmer. However, additional hints from developers could enab= le even further analysis, or enable vendors to add analysis in compilers at= lower expense. In the example like the following, a compiler can fairly ea= sily detect that a potential UB is at hand:

int* produce()
{
  if (cond) return &global;
  else      return nullptr;
}

void consume(int* p)
{
  use(*p);
}

consume(produce());

But even here, certain problems occur. What if the two functions are com= piled separately; e.g., if produce is part of a separate third= party library? Even if compiler performs a per-file analysis, it may not h= ave sufficient resources (RAM) to perform a global link-time analysis. Even= if the analysis is successful and detects a potential UB, it doesn't tell = us who of the three: author of produce, author of consum= e or the guy who assembles them, is responsible for the situation an= d 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= ..

Also, as shown in the example with sqrt it is sometimes not= possible to tell from only observing the reads from a variable what the fu= nction's requirement is. In the case of sqrt it is not the UB = that we want to avoid but an infinite recursion.

Another reason where assisting the static analysis may prove useful is w= hen there is more than one way to express a given condition. Consider the f= ollowing code:

class Vector
{
  const T& front() const; // requires: !this->empty()
  // ...
};

void test(Vector & vec)
{
  if (vec.size() !=3D 0)
    use(vec.front());
}

You know that vec.size() !=3D 0 and !vec.empty() mean the same thing, but compiler may not, especially if it cannot look = inside the definitions of member functions (because they are compiled separ= ately).

How long does a condition hold?

We illustrate the issue in question with the following two examples.

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)
}

Assuming that a static analyser can somehow figure out that sort leaves elements in the state that satisfies the condition is_so= rted, can it be sure that the condition still holds when fun is finished? After all fun could be manipulating iterato= rs that alias b and e. Apparently, static analysi= s cannot give us a 100% bug-free guarantee. It can only helps detect certai= n bugs.

Second, it is obvious that a certain condition does not last forever. Ho= w is the analyser supposed to know when a given condition ceases to hold? O= ne easy answer would be to say that when a non-const operation= is called on the object all conditions it might have satisfied are now co= nsidered not satisfied. But this would break even simple use cases:

void test(std::vector<int> & vec)
auto b =3D vec.begin(); // non-const: invalidates all conditions
auto e =3D vec.end();   // non-const: invalidates all conditions
std::sort(b, e);      // requires: valid_range(b, e)

Even if the analyser knows that vec.begin() and vec.e= nd() form a valid range, they are a non-const operation= s and invalidate any assumptions about their value/state. Any language feat= ure for assisting static analysis must provide a way of specifying which op= erations invalidate which conditions. But this is likely to make the specif= ications very complicated, and discourage everybody from using the feature.=

"Properties": a hypothetical language feature

In this section we describe a language feature that would enable definin= g value constraints in a somewhat different way than the "imperative" appro= ach described in [N1962]. We call it properties<= /em>, which have been described in [N3351]. A proper= ty 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 keyw= ord "property":

template <typename T>
property bool is_non_empty (std::vector<T>);

A property is something that an object, or a group of objects can acquir= e 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:

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 =3D back(); // required property is present
v.pop_back();   // looses property is_non_empty

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 discar= ds all its properties. But this would imply that in our case even calling <= code>back() discards the property, so a more complex way of specifyi= ng how the properties are preserved may be required.

So, what do we buy using properties rather than considering any boolean = expression such a property? First, properties are pure: they have no side e= ffects. Second, we can express value constraints that are not expressible w= ith expressions:

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());

We do not propose to add such properties to the language. We just want t= o show a different perspective on value constraints. [N1= 962] also offers this perspective, but we fear that the focus on broken= contract handlers and the order of evaluation of different value constrain= ts, 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.

Interactions with other C++ features

When should precondition hold?

A common answer to this question is "after function parameters have been= initialized, before its first instruction is executed." While it looks goo= d in typical simple examples, consider the following case:

void fun(Tool * const tool, int const i)
// requires: tool !=3D nullptr
// requires: tool->value() >=3D 0;
{
  line_1: int j =3D transform(i);=20
  line_2: int k =3D process(tool->value());
}

A precondition constrains the state of a remote object of type Too= l, 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 line_1, we will now proce= ed to instruction line_2. It is only now that we really need t= he precondition to hold, but by now the state of the remote object referred= to by pointer tool might have already changed (perhaps functi= on transform modified it). While the precondition held = upon entry, the same condition caused a UB later on. Even if one argues tha= t function must not break the precondition itself, one should still conside= r the possibility that while executing line_1 another thread m= ay concurrently update the object referred to by tool. So, sho= uld precondition hold for the entire duration of its function? Or is it a b= ad idea to express a constrain on remote objects that we do not obtain by v= alue? 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: t= hey obtain and return iterators, which are handles to remote parts likely a= liased and accessible by other threads.

constexpr functions and literal types

constexpr functions can be evaluated at run-time or at comp= ile-time. Ideally, a compile-time evaluation of such function should result= in compile-time error when its precondition or postcondition is broken. Th= is is possible if expressions in preconditions and postconditions are core = constant expressions. It appears reasonable to require that constexpr= functions have only constexpr value constraints.

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/mov= e constexpr constructor. This constructor can be used to creat= e a compile-time constant, whose invariant is expected to hold. This may re= quire that the invariant should also be constexpr, as otherwis= e it is impossible to verify it at compile time. On the other hand, the int= erface of user-defined literal types can be divided into compile-time (constexpr) and run-time part. The effects of the other one may alt= er other parts of the program state that may only be invariant-verified wit= h run-time expressions. More, some constructors are constexpr = even for non-literal classes: their purpose is to guarantee the static init= ialization of global objects. It is not clear if this should affect the constexpr requirement on the class invariant.

When should invariant hold?

When is class invariant supposed to hold? Objects are manipulated via cl= ass's public interface. Public functions often need to compromise the invar= iant, but they always put the invariant back when they finish -- even via a= n exception. This means that as long as no function from the object's publi= c interface is being invoked on it, or any of its subobjects manipulated, t= he object's invariant should hold.

=20

This is different from the common notion that invariants should hold bef= ore 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.

Composing invariants

Given some class D, apart from its "direct" invariant, we e= xpect that invariants of D's bases classes and D'= s data members also hold. This can be implicit, you do not have to make rec= ursive definitions yourself, similarly like you do not have to specify in t= he destructor which subobject's destructors need to be called. But this doe= s not cover all cases. Consider class optional (similar to Boo= st.Optional), it can be implemented as follows: 

template <typename T>
class optional
{
  bool is_initiailzed_ =3D 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*() {=20
    assert (is_initiailzed_);
    return *storage();=20
  }
  optional(const T& v) {
    new (storage()) T(v);=20
    is_initiailzed_ =3D true;
   }
  ~optional() {=20
    if (is_initiailzed_)
      storage()->T::~T();
  }=20
}; =20

Obviously, we store (sometimes) an object of type T inside, bu= t 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 co= mpiler may not be able to deduce it. We might need to express a "conditiona= l" invariant:

// invariant: !is_initialized_ || invariant(*storage());

Similarly, a vector of Ts (std::vector<T>) can be thought of as being composed of the Ts it contains. = This is reflected in how its equality comparison is defined and how const-n= ess is propagated. A value of the container is composed of the values of it= s elements. In a similar manner, we would like to be able to express invari= ants 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 access= ible from the vector, its invariant must hold. But will the machine know th= at the result of vec.back() should have its invariant hold? af= ter all, calling back() is not always allowed, and may render = a UB.

Another open question is if we should check invariants of member subobje= cts if they are references (and therefore do not pertain to the master obje= ct=E2=80=99s value).

Function's public interface

For the purpose of specifying the semantics of value constrains, we may = need to redefine the concept of class's public interface. Consider the foll= owing definition:

class Account
{
public:
  void modify(Param p);
  friend void swap(Account& a1, Account& a2);
private:
  // ...
};

Function swap, although it is not a public member function,= clearly is part of Account's public interface. I.e., we allow= that it temporarily breaks the invariant of objects a1 and a2. The technique with defining operator-like free functions as = friends is not just a trick. In fact it is sometimes recommended for operat= ors like operator=3D=3D when the two arguments are to be treat= ed symmetrically.

Protected members

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 he= rself.

On the other hand, protected functions may also need to specify their pr= econditions as they constitute an interface for deriving classes (which can= also be considered users), and for them calling other protected members ap= pears reasonable.

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 mem= bers, but they still may require something. Not suer if this use case is wo= rth complicating the language.

Constraining STL

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 ab= le to handle them, but consider it rather a test of expressive power. The g= oal is to help determine where we want to stop in expressing the semantics = in the language.

=20

Case 1: a valid range

This is probably the most difficult one to handle. Nearly any algorithm = on STL ranges requires that end is reachable from 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 c.begin() and c.end() called on any STL container form= a valid range. Is a value constraints framework capable of expressing that= the values of c.begin() and c.end() satisfy the = requirements of, say, std::for_each?

Case 2: sub-ranges

Similarly, in the call m =3D std::find_if(b, e, p), assuming t= hat b and e form a valid range, can it be verifie= d or even expressed that b and m as well as m and e form valid ranges and that these combinations = should satisfy the requirement of subsequent STL algorithms about valid ran= ges?

Case 3: sorting

Consider functions sort and binary_search 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 g= iven predicate. The later requires that the range is partitioned w= ith 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 operator< = but is not sorted.

Solution with properties and axioms

Below we show how the above task can be solved with sophisticated features = like properties (described above) and axioms (similar to those described in= [N2887]).

Case 1

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); };
 =20
vector<int> v =3D {/*...*/};
sort(v.begin(), v.end());
=20

Case 2

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
};

vecotr<int> v =3D {/*...*/};
auto i =3D find(v.begin(), v.end(), 7); // axiom vec_range
auto j =3D find(i, v.end(), 7);         // postcondition of find

Case 3

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 !c=
mp(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) =3D> 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) };

Again, we do not propose to standardize the above, but we show that prec= onditions in STL algorithms are expressible with a sufficiently complex fa= cility.

=20

What do we need to standardize?

The language feature of value constraints can be divided into two main p= arts. (1) What value constraints we define and how, (2) how do we handle ru= n-time response to a broken value constraint.

Defining value constraints

At this point it is too early to decide on the details, but one thing ap= pears fairly uncontroversial. Value constraints support needs two accommoda= te two fairly opposite requirements: (1) no run-time overhead in cases like= (operator[] for vectors), (2) guaranteed (in certain situati= ons) evaluation of the predicates (where performance requirement is not cri= tical).

This calls for the following semantics. If a piece of code that "relies"= on a value constraint is executed, and its corresponding value constraint = would return false if it were evaluated (but no evaluation is requ= ired), the behaviour of the program is undefined. Any value constraint "in = its proper moment" may be evaluated once or not evaluated -- it is unsp= ecified.

Run-time response

One option is not to standardize what should happen when we detect at ru= n-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. W= ith this approach a minimum conforming implementation only needs to syntax-= and type-check the declarations.

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 = T satisfies some requirements", or "this constraint has comple= xity O(N), evaluate it only when O(N) and bigger complexities are enabled",= or "never evaluate this".

Acknowledgements

Lots of content in this paper is inspired by work in = [N1962], [N2887] and [N3351]<= /a>.

Gabriel Dos Reis suggested the "STL test" for a precondition framework.<= /p>

References

 ------=_Part_80_32937670.1404485523485-- .