5 thoughts on “GotW #99: Postconditions (Difficulty: 7/10)”

1. Questions
   2. Rewrite the example in Question 1 to show how to approximate the same effect using assertions in today’s C++. Are there any drawbacks to your solution compared to having language support for postconditions?

   Hmm – I could use macros – like this:

   “`
   #if _NDEBUG
   #define POST_ASSERT(cond, …) { \
   auto _return_ = [&] __VA_ARGS__ (); \
   assert(cond); \
   return _return_; \
   }
   #else
   __VA_ARGS__
   #endif
   “`

   And usage:

   “`
   string combine_and_decorate( const string& x, const string& y )
   POST_ASSERT(_return_.size() > x.size() + y.size(),
   {
   if (x.empty()) {
   return “[missing] ” + y + optional_suffix();
   } else {
   return x + ‘ ‘ + y + something_computed_from(x);
   }
   })
   “`
   So – not so much trouble for this example – just enclose body of your function with POST_ASSERT(condition, /*body here*/ )

   3. Should a postcondition be expected to be true if the function throws an exception back to the caller? Justify your answer with example(s).

   IMHO – it should be special treating of throw here – maybes reintroduce throws to C++ and special meaning of && and || here – like

   “`
   int* allocate(int size)
   [[post(_return_ != null || throws std::bad_alloc)]]
   {
   return new int[20];
   }
   “`

   4. Should a postcondition be able to refer to both the initial (on entry) and final (on exit) value of a parameter, if those could be different? If so, give an example.

   No – the exit criteria should refer to values at the exit of function. So – take the final values of “output” parameters.
   That’s just my opinion – I hate out-params…

2. 1. A postcondition is a guarantee made about the program state upon completion of the function’s execution. It may involve the return value, or changes made to by-reference arguments, or (for member functions) the state of the object, or even the state of the program (global and other static variables).

   You can express postconditions with assertions, but you have to be careful about the scope. If the destructors of locals and by-value parameters can affect the postcondition, you might have to wrap everything to ensure the assertions run after the function rather than just before the end of the function.

   2. One way to enforce the postcondition with an assertion would be to rename the existing function to combine_and_decorate_impl, and add:

   [CODE]
   std::string combine_and_decorate(const std::string &x, const std::string &y) {
   auto result = combine_and_decorate_impl(x, y);
   assert(result.size() > x.size() + y.size());
   return result;
   }
   [/CODE]

   A disadvantage is that the postcondition isn’t expressed directly alongside the implementation.

   3. Postconditions may not hold if an exception is thrown, since the function did not complete its execution.

   In the combine_and_decorate example, if a string concatenation results in a std::bad_alloc exception, the function does not complete and the return value is unspecified. Thus it’s impossible for the postcondition to be satisfied. There’s no point in reporting a postcondition violation if there’s already an exception in flight. The exception is propagated up to any level that catches it. And, if nothing catches the exception, then the stack unwinding doesn’t even happen and the program terminates, further showing that it’s not useful to enforce postconditions when there’s an exception.

   On the other hand, it would be nice to be able to use a postcondition to ensure the a function is thread safe.

   4. It might be nice to have the ability to refer to the initial value of a parameter when checking a postcondition, but, in the general case, it would open a Pandora’s box. Saving the initial value of a parameter that might change requires making a copy. What if copies are expensive? What if the copy constructor has side effects? What if the parameter is of a type that’s intentionally designed to make shallow copies? What about slicing if the parameter is a pointer or reference to a base class? What if it’s a move-only object?

3. 1. A postcondition is a binary predicate that must evaluate to true at every return point of a function. It is a special case of assertion. In the example, the postcondition is evaluated whether x is empty or not.

   2. One way to emulate it is getting back to the single point of return :
   std::string ret;
   if (x.empty()) {
   ret = “[missing] ” + y + optional_suffix();
   } else {
   ret = x + ‘ ‘ + y + something_computed_from(x);
   }
   assert(ret.size() > x.size() + y.size());
   return ret;

   It has the usual drawbacks of single return point functions.

   Another way would be use scoped_guards to defer the execution of the evaluation, but it has some quirks, since they would be executed in case of exceptions (or special care shall be taken to ensure not), where the postcondition may not make sense (see below).

   3. In the general case, no. The postcondition may refer to values that are not even available in the case of exceptions (the return value of the function, for example). So its evaluation would not even be possible (this is the case in the article example if std::bad_alloc is raised by the concatenation). Also, there is a need to express that a postcondition cannot be met for some reasons (usually, resource exhaustion or environment), and exceptions are the language standard feature to express this (operator new has a postcondition that the memory has been allocated, and fails with an exception if it can’t guarantee it).

   However, there are cases where we maintain some guarantees even in the case of exceptions (strong exception guarantees). There would be some benefit to expose such guarantees as part of the postconditions of the function. An exception-safe swap can guarantee that, in case of failure, its arguments are unchanged. It contradicts the standard postcondition, but it is an important property, that is in fact part of the contract between the caller (i expect you to either succeed, or not modify the arguments) and the callee, who is bound by the contract.

   4. Yes. A simple case where this would be required to express the postcondition is (using pseudo-syntax)
   void inplace_dup(std::string& str)
   [[post( str@exit.size() == str@entry.size() * 2)]]
   {
   str = str + str;
   }

4. 1. A post condition checks to ensure that a certain invariant of an operation/transform is maintained. This is similar to assertions which check that the inputs to an operation satisfy certain conditions. In the example code, an invariant of the operation of concatenating two strings (with possible extra annotations) is that the output must be longer than the combination of both inputs.

   2.

   string combine_and_decorate( const string& x, const string& y )
   {
   string res;
   if (x.empty()) {
   res = “[missing] ” + y + optional_suffix();
   } else {
   res = x + ‘ ‘ + y + something_computed_from(x);
   }
   assert(res.size() > x.size() + y.size());
   return res;
   }

   The disadvantage of this approach is that you must have a copy of the post condition at every possible normal function return path. If the method was something like summarize_and_decorate it would be nice to have separate post conditions for the different return paths, for example:

   string summarize_and_decorate( const string& x, const string& y )
   {
   string res;
   if (x.size() > max_length) {
   res = “[long x] ” + y + optional_suffix();
   assert(res.size() > y.size());
   } else {
   res = x + ‘ ‘ + y + something_computed_from(x);
   assert(res.size() > x.size() + y.size());
   }
   return res;
   }

   However, I think standard assertion syntax is perfectly well suited to handling this case.

   3. No, when an exception or other error condition is expected to be handled by the caller the return result is not expected to be well formed. In this case, checking the post condition makes no sense.

   One example is the square root function restricted to the real domain:

   real checked_sqrt(real arg) [[post( _return_ >= 0)]]
   {
   assert(arg >= 0);
   return sqrt(arg);
   }

   Given a negative arg, there is no reasonable real number to represent the output.

   4. I think some kind of syntax which mimics lambda captures would be the best way to acquire necessary prior values rather than having the compiler perform a generic copy of the initial value. I think this form would not only perform better and be more generic, but ultimately be easier to read and write.

   An example (not exactly legal C++ code, but hopefully this gets the idea across):

   void append_suffix_and_decorate(vector& args, const string& suffix) [[capture(vector prev_sizes = get_current_sizes(args)), post(args[i].size() >= prev_sizes[i] + second.size())]]
   {
   for(string& arg : args)
   {
   if(arg.empty()) {
   arg = “[empty] ” + suffix;
   }
   else {
   arg += suffix;
   }
   }
   }

   I think the advantage of this over using regular assertions and C++ code to get the same effect is that the cost of acquiring prev_sizes can be omitted in a release environment without having macro-like exclusion code everywhere.
   In this example it’s easy enough to avoid this anyways, but I’m not sure if this is true for more complex in-place transformations.

5. 1. As I interpret the example, it’s an assertion that is tested after the return value has been constructed, but before control has transferred back to the caller.

   2. This is apparently in experimental, but you could imagine using any sort of “run this on exiting scope” primitive:

   
   #include <cassert>
   #include <experimental/scope>
   using std::experimental::scope_exit;  // I think that's correct.
   
   string combine_and_decorate( const string& x, const string& y )
   {
       string _return_;
       scope_exit([&]() {
           assert(_return_.size() > x.size() + y.size());  // or throw, or what-have-you
       });
       if (x.empty()) {
           _return_ = "[missing] " + y + optional_suffix();
       } else {
           _return_ = x + ' ' + y + something_computed_from(x);
       }
       return _return_;
   }
   

   Drawback: This structure forces you to put the return value in an explicit variable that’s captured in a lambda by reference. In my rewrite, the code now returns from a single point rather than multiple points, but that wasn’t really necessary.

   If you have more complex return paths, then you might want to go a different route, and put the entire function body in a lambda (ick) and test the post condition in the main function itself rather than relying on scope-exit to trigger a post-condition check.

   3. It depends on the post-condition. For example, if you’re checking that a function upholds the strong exception guarantee with a post-condition, then you have a post-condition to check in case of an exception.

   
   void vector<T>::push_back(const T& item) : try {
     // push back
   } catch {
     // check that this->size() is unchanged
     throw;
   }
   

   4. See previous example of verifying that strong exception guarantee was upheld on std::vector::push_back() triggering an exception.

Comments are closed.