A Proof of Correctness is a mathematical proof that a computer program, or a part thereof, will yield correct results, i.e. results fulfilling specific requirements, when executed.
Before proving a program correct, the theorem to be proved must be formulated. The hypothesis of such a correctness theorem is typically a condition called a pre-condition, that the relevant program variables must satisfy immediately before the program is executed. The thesis of the correctness theorem is typically a condition called a post-condition, that the relevant program variables must satisfy immediately after the execution of the program. The thesis of a correctness theorem may be a statement that the final values of the program variables are a particular function of their initial values.