A set of criteria that must be true upon completion of the execution of a use case.

One or more conditions that are guaranteed to be true on the completion of a method’s execution, assuming that its preconditions are true.