标签：#formalmethods

Here is every promise a to-do list makes. VARIABLE tasks Init == tasks = [i \in Ids |-> "absent"] Add(i) == tasks[i] = "absent" /\ tasks' = [tasks EXCEPT ![i] = "open"] Complete(i) == tasks[i] = "open" /\ tasks' = [tasks EXCEPT ![i] = "done"] Reopen(i) == tasks[i] = "done" /\ tasks' = [tasks EXCEPT ![i] = "open"] Delete(i) == tasks[i] # "absent" /\ tasks' = [tasks EXCEPT ![i] = "absent"] ClearCompleted == /\ \E i \in Ids : tasks[i] = "done" /\ tasks' = [i \in Ids |-> IF tasks[i] = "done" THEN "absent" ELSE tasks[i]] Not a summary. Not the important ones. All of them. A task cannot go from absent straight to done. Clearing completed items leaves the open ones alone. You cannot delete something that was never there. Nine lines, and when you've read them you have read the entire contract. Now go find that list for the system you work on. You can't. It doesn't exist. It's distributed across a test suite that asserts outcomes rather than rules, some validation scattered through handlers, and the memory of whoever's been there longest. The guarantees are real — your users depend on every one of them — and there is no file you can open to see them. That's the gap I want to talk about, because you can close it in an afternoon, and because something has changed recently that makes closing it pay for itself. The prime mark and two operators That's most of the syntax, so let's get it out of the way. tasks' means "tasks, in the next state." /\ is and . \E is "there exists." A definition like Complete(i) is a formula relating the current state to the next one — read it out loud: the task is open, and afterwards it is done. That's it. That's the language, near enough, for this purpose. The real file adds about eight lines of scaffolding around what you saw: a module header, a TypeOK saying a task is always in exactly one of the three states, and the two lines that tie the actions together — Next == \/ \E i \in Ids : Add(i) \/ Complete(i) \/ Reopen(i) \/ Delete(i) \/ ClearComplete