preconditions and postconditions

Before you can prove a program 'correct', you have to say what correct means — and that depends on what you are allowed to assume about the input and what you owe about the output. A precondition is the promise the caller makes about the input ('the array is sorted', 'n >= 0', 'the list is non-empty'). A postcondition is the promise the procedure makes about the result given that input ('returns the index of x, or -1 if absent'; 'the array is now sorted and a permutation of the original'). Together they form a contract: assume the precondition, deliver the postcondition.

Correctness is always relative to this contract. Binary search is correct only under the precondition that its input array is sorted; run it on an unsorted array and a 'wrong' answer is not the algorithm's fault — the caller broke the contract. The postcondition is what your invariant/induction proof must establish at the end, and the precondition is what you are entitled to assume at the start. For a sort, a careful postcondition has two halves people often forget: the output must be sorted AND be a rearrangement (permutation) of the input — a procedure that outputs a sorted list of zeros is 'sorted' but wrong.

Writing these conditions down is half the battle, because vague specs hide bugs. They also compose: when one procedure calls another, the caller must ensure the callee's precondition holds, and may then rely on the callee's postcondition. This is exactly how the combine step in a recursive proof works — the recursive call's postcondition is the hypothesis you reason from. The honest caveat: a proof only certifies the code against the stated postcondition; if the postcondition itself fails to capture what you actually wanted, you can have a flawless proof of the wrong thing.