Some thoughts on good spec properties
Lots of updates this week! First of all, my talk Is Software Engineering Real Engineering is now available online! It's the video version of the crossover project. Link is to the video, slides, references, and FAQ. I know a lot of people have been waiting for this; I hope it lives up to expectations :)
Second, the TLA+ workshop is on Monday! There's still a couple slots if you want to sign up; use the code C0MPUT3RTHINGS for 15% off.
Like with any discipline, using TLA+ (and formal methods more broadly) takes a lot of different skills. One of them is choosing good properties to verify. I want to explore what we mean by "good properties". Let's take a real simple model of wire transfers:
EXTENDS TLC, Integers
CONSTANTS People, NumTransfers
Money == 1..10
(* --algorithm wire
variables
acct \in [People -> Money];
define
NoOverdrafts == "???"
end define;
process wire \in 1..NumTransfers
variable
amnt \in 1..5;
from \in People;
to \in People;
ready = FALSE;
begin
Check:
if acct[from] >= amnt then
ready := TRUE;
Deposit:
acct[to] := acct[to] + amnt;
Withdraw:
acct[from] := acct[from] - amnt;
ready := FALSE;
end if;
end process;
end algorithm; *)
The bug here is that if we do two wires, they can race each other past the Check clause and leave someone with a negative balance. We want to write NoOverdrafts to catch this error.
There's two ways to do that. We can say that ready => (acct[from] >= amnt) {1}.1 We can also say that acct[from] >= 0 {2}. Notice they'll both fail for the same behavior of two concurrent wires, but {1} will fail a couple of steps earlier and give a shorter error trace. In my experience, that makes {1} closer to how we think about good programming practices: make errors appear as early as possible.
But I'd argue that {2} is a better property for specification:
-
{1} says the bad thing is very likely to happen, but it's not guaranteed.2
-
{1} is an internal property while {2} is external. An outsider observer can't see the value of
readybut they can see ifacctis negative. So {2} being violated can actually have downstream effects on the external world, which makes it more important. -
{2} is mathematically stronger. Right now we only have one type of action in this system,
Wire, but complex systems have lots of different actions. Model checkers are looking for a worst-case scenario across all sequences of actions, and that might not include aWireaction. So {2} will automatically catch things that {1} misses.
Note that writing {1} can still make sense, since it'll fail earlier with a shorter error trace. But {1} is only useful if you also have {2}. My point is that in specifications the broader properties are "more important" than narrow ones. Beginners to FM tend to write narrow properties because they're used to writing narrow tests, and that's something they have to unlearn.
Why the difference? Most people run test suites as part of their coding process, so they want the suite to run quickly. That puts lots of constraints on what you can easily check. Model checking a specification usually happens separately, so isn't as tightly time-constrained. Broader properties make sense.
On writing that, I wonder if I should think of {1} as a "regression properties" kinda similar to a regression test. IE only write {1} after I see {2} fail and see the error trace, as a way of more quickly debugging regressions in the spec.
Pulling this all together. Some heuristics for good properties:
- Represent an actual failure in the system, not just the potential for failure
- Are observable differences in the external state, not the internal state
- Are broad enough to cover many different narrower properties
In conclusion, I just realized I have like a million more proto-thoughts on TLA+ and the nature of specification all bouncing around inside. Maybe for a future newsletter.
If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.
My new book, Logic for Programmers, is now in early access! Get it here.