Specification Refinement

When teaching formal methods, I often get asked how we can connect the specifications we write to the code we produce. One way we do this is with refinement. All examples are in TLA+. Imagine we’re designing a multithreaded counter. We don’t know how we’re going to implement it yet, so we start by specifying the abstract behavior.1 ---- MODULE abstract ---- EXTENDS Integers, Sequences VARIABLES pc, counter vars == <<pc, counter>> \* Two threads Threads == 1....

Submit