Precondition

The precondition of a function or program that specifies the conditions under which the behavior of the function is defined. The precondition is part of the formal specification of the function ( or program ) and is used to verify: If it applies, all postconditions must be satisfied after execution of the function, otherwise the program is not correct.

The concept of pre-and postconditions is used mainly in formal semantics: it is the basis of the axiomatic semantics Represents the aim is, from the pre-and postconditions of each part of the program logically the desired postcondition for the entire program to conclude.