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
4 pages link to PreCondition: