An algorithm is correct when it satisfies its specification for every input covered by that specification.

A correctness argument separates two questions:

• partial correctness: if the algorithm terminates, does its result satisfy the required postcondition?
• termination: does the algorithm actually finish for every allowed input?

Together they establish total correctness.

Proofs typically identify properties preserved by each step, reduce the problem to smaller valid instances, or show that every possible case is handled correctly.

Correctness and efficiency are separate properties. An algorithm may be fast but wrong, or correct but impractically slow.

Making assumptions, inputs and required outputs explicit is therefore part of reasoning about an algorithm, not merely documentation around it.