Penguin

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