postcondition incorrectly characterized #1095
Description
What is the problem?
In the section on defensive programming there's a statement
A postcondition is something that the function guarantees is true when it finishes.
But a postcondition only needs to hold upon termination if the precondition was true on entry. That qualification is missing.