Prove that a program meets its specification.
Correctness specification: formal description of how program is supposed to behave
Program is correct: its executions satisfy the specification
Prove statements of form {precondition} program {postcondition}
Partial correctness: if program starts satisfying φ, and if it halts, then when it halts ψ is satisfied
Total correctness: partially correct, and terminates whenever started while satisfying φ