In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.
Preconditions that are missing, insufficient, or not formally proved (or have an incorrect attempted proof), or are not checked statically or dynamically, can give rise to Security problems, particularly in unsafe languages that are not strongly typed.
In addition where numeric types have a limited range (as they do in most programming languages) the precondition must also specify the maximum value that the parameter may have if overflow is not to occur.
Where the language supports range sub-types (e.g. Ada) such constraints can be automatically verified by the type system.
[1] The routine in the following example written in Eiffel takes as an argument an integer which must be a valid value for an hour of the day, i. e., 0 through 23, inclusively.