Correctness

Correctness of Iterative and Recursive functions

A program is said to be correct, if it produces a correct output on every acceptable input, which, in terms of the proof terminology, means that for all possible inputs that satisfy the precondition, the program produces an output that satisfies the postcondition.

Precondition: an assertion that states what must be true before the program starts execution
Postcondition: an assertion that states what must be true when the program ends
                       - in particular, it can describe what is a correct output for the given input.

if a program meets both precondition and postcondition, then we say the program is correct.

Partial Correctness
- prove that if the precondition holds before the program starts then the following is true at the end of each iteration of the loop.





Loop Invariant 
- a statement that is true on entry into a loop and that is guaranteed to remain true at the end of every iteration of a loop.