Penguin

A logical condition that must hold before a method of function can be called. Used to generated proofs about program behaviour. Supported natively in the Eiffel language.

See also PostCondition