July 2004
Intermediate to advanced
752 pages
35h 59m
English
A constraint that must be true at the completion of an operation.
A postcondition is a Boolean expression that must be true after the execution of an operation completes. It is an assertion, not an executable statement. Depending on the exact form of the expression, it might be possible to verify it automatically in advance. It can be useful to test the postcondition after the operation, but this is in the nature of debugging a program. The condition is supposed to be true, and anything else is a programming error. A postcondition is a constraint on the implementor of an operation. If it is not satisfied, then the operation has been implemented incorrectly.
See also invariant, precondition.
A postconditions is ...
Read now
Unlock full access