Binding of postcondition variables
The current approach is to type the return value variable the same as the function; this creates new objects for functions returning prvalues. We'd like the function's return value to propagate through the sequence of postconditions without creating new objects, if possible.
For functions returning prvalue class types, we probably want to bind result variables using rvalue references. For everything else, I think it's reasonable to return by decayed value.