Prefer `Ensures()` for expressing postconditions

Reason

To make it clear that the condition is a postcondition and to enable tool use.

Example

void f()
{
    char buffer[MAX];
    // ...
    memset(buffer, 0, MAX);
    Ensures(buffer[0] == 0);
}

Note

Postconditions can be stated in many ways, including comments, if-statements, and assert(). This can make them hard to distinguish from ordinary code, hard to update, hard to manipulate by tools, and might have the wrong semantics.

Alternative: Postconditions of the form "this resource must be released" are best expressed by RAII.

Note

Ideally, that Ensures should be part of the interface, but that's not easily done. For now, we place it in the definition (function body). Once language support becomes available (e.g., see the contract proposal) we will adopt the standard version of preconditions, postconditions, and assertions.

Enforcement

(Not enforceable) Finding the variety of ways postconditions can be asserted is not feasible. Warning about those that can be easily identified (assert()) has questionable value in the absence of a language facility.