3 Pre and post conditions

A pre condition is simply ``what we know before the execution of a statement in a program.'' A post condition is ``what we know after the execution of a statement in a program.'' The analysis of the pre and post conditions of a program is essential, because we can prove the correctness of a program (or an algorithm) rigorously.

If you consider an algorithm, the pre condition of the entire algorithm is what is given to the program. The post condition of an entire algorithm is the outcome of a program. Being able to mathematically derive the post condition of an algorithm based on its pre condition means we can prove whether an algorithm does what it is supposed to. There is no need to use test cases anymore, because a proof of correctness covers all cases that can be thrown at the algorithm.