Wrap up: Little proofs

Wrap up of “To be a better programmer, write little proofs in your head”.

Monotonicity

• Which parts are monotonic?
• Which parts are immutable?

Pre-/post-conditions

• Asserts about the (program’s) state.
• At the beginning/end of procedures.

Invariants

• Must be true before/during/after the code run.

Isolation

• Which parts are affected by a change to the code?

Induction

• Repeating by recursion.
• Look for base step, recursive step.

Write provable code

• Make it easy to make little proofs.