Precondition (computer science)
The precondition of a function or a program indicates the conditions under which the behavior of the function is defined. The precondition is part of the formal specification of the function (or the program) and is used for verification : If it applies, all postconditions must be fulfilled after the function has been executed , otherwise the program is not correct .
The concept of pre- and post-conditions is mainly used in formal semantics : it represents the basis of axiomatic semantics . The goal is to logically create the desired post-condition for the entire program from the pre- and post-conditions of the individual parts of the program to infer .