• 4.6: Loop Invariants

    • Massachusetts Institute of Technology: Srini Devadas and Eric Lehman's "Induction III" URL

      Read Section 3.2. The reading presents a proof that an initial configuration of the 9-number puzzle cannot be transformed into its inverse. The proof uses the fact that after each move the number of inversions remains even; this is an invariant. Invariants are used in proofs and in proving the correctness of programs.

      Invariants are only introduced in this course; they are covered in detail in programming language courses.