Postcondition (computer science)
The postconditions of a function or a program indicate which statements must apply after execution if the preconditions were met beforehand . The postcondition is part of the formal specification of the function (or the program) and is used for verification : If the precondition 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 .
Postconditions also play an important role in the less formal testing of software, as the result of test runs can easily be compared with the postconditions. This is mainly used for the so-called unit test .