The Invariant Game, or how to reason effectively about iterative programs

Presenter: Matteo Vaccari

Objective: To get a better understanding of iterative programs.  To sharpen the skill in understanding how to solve problems with "while" loops; even concurrent "while" loops.

Intended audience and prerequisites: This session is for developers; experience with Agile methods or TDD is not required.  At the same time it should be of interest to people experienced in Agile engineering practices; the Invariant Technique could be for them a novel, different direction of improvement.  We will not use computers, just paper, pencil and imagination.

Contents:

TDD is an excellent technique for designing programs; it's easy to define, but takes time to master.  One of the difficulties is in bridging the gap from "red" to "green", that is how to "guess" a first solution to a problem.  Another difficulty is finding ways to simplify (that is, refactor) a working program.

The Invariant Technique can sharpen your skill in overcoming both of the above difficulties.

Most interesting programs are iterative.  One way to understand how a loop solves a problem is to find an invariant. An invariant is a boolean expression that is true before entering the loop, is preserved by the body of the loop, and therefore must be true when (and if) the loop terminates.  The "and" of the invariant and the negation of the loop boolean condition must then imply the postcondition that we require.

We'll learn what an invariant is, and how it explains the meaning of a loop.

We'll learn a few simple heuristics to find useful invariants.

We'll learn how to solve simple programming problems with simple, crisp and terse programs.

Format and length: Workshop, 90 min