= Algorithm correctness
<Partial correctness> means that, if the <algorithm> terminates on a permitted <input>, its <output> meets the <formal specification>. <Total correctness> additionally requires <algorithm termination> on every permitted <input>.
A <precondition> $P$ describes permitted starting circumstances; a <postcondition> $Q$ describes the required result. <Partial correctness> says that starting with $P$ and finishing implies $Q$. <Total correctness> also guarantees finishing. A <loop invariant> supplies the connection between these conditions during repeated steps.<CS 2112 Fall 2019/Loop invariants>[CS 2112 Fall 2019; Loop invariants, Using loop invariants to show code is correct: Establishment, Preservation, Postcondition, and Termination]{ref}
Correctness is relative to a <formal specification>. Returning the first entry of an <array> correctly implements "return the first entry", but fails "return the <maximum>" on $[3,1,4,4,2]$. A fast wrong answer does not acquire <algorithm correctness> from its <time complexity>. Numerical closeness matters only when the <formal specification> allows an approximation. <Software testing> and <test coverage> provide evidence about selected executions; they do not by themselves establish <algorithm correctness> for every permitted <input>.
Back to article page
