Correct Programming

lecture
java
specification
correctness
loop-invariants
hoare-logic

See csse2002 for course logistics. Lecture by Dr. Brae Webb.

Correctness is the prime quality. If a system does not do what it is supposed to do, everything else about it […] matters little.

— Bertrand Meyer, Object-Oriented Software Construction, §1.2 p.4, 1997

Today’s outline

  1. Specification — what does it mean for a program to be correct?
  2. Deriving preconditions — propagating a postcondition backward through code
  3. Loop invariants — reasoning about (and designing) loops
  4. Pragmatic considerations — when is this worth the effort?

All content is in java-hoare-logic and java-loop-invariants.

Applied class

See week12-tutorial-lambdas-and-streams — more practice with lambdas and streams, extending java-lambdas-and-streams (Week 11).

Practical

See week12-lab-generics — more practice with bounded generics and wildcards, extending java-generics (Week 9).

Next steps

  • CSSE3100 — Reasoning About Programs
  • Floyd, 1967 — Assigning Meanings to Programs
  • Hoare, 1969 — introduced the triple \(\{P\}\,S\,\{Q\}\)
  • Dijkstra, 1975 — weakest-precondition reasoning