A logical condition that will hold after a method of function has completed. Used to generated proofs about program behaviour. Supported natively in the Eiffel language.
See also PreCondition
3 pages link to PostCondition:
