Using a journaled file system operation refinement, the authors of this paper assert that future software development should be centered around readable documentation containing rigorous high-level mathematical specifications and calculations, and supported by validation and verification tools interoperating directly with this mathematical content. This future has not yet arrived, but as a plausible approximation, they present, in the style of the Algebra of Programming (AoP), a set of concise relation-algebraic formalizations and calculations that were validated using the relational model checker Alloy, which understands specifications in a closely related language.

After a quick but thorough introduction to these formalisms, they are put to work on the delete operation in a journaled (flash) file system motivated by the verified file system challenge [1].

Two nonfunctional requirements influence the development. The first is that the relevant in-memory index can be reconstructed from the journal after power loss, which turns into a concrete state invariant during the refinement. The second requires wear leveling, and is addressed in the design by replacing block overwrite operations with new block allocations and recording these in the journal.

This leads to the cost of the most complex calculations presented in the paper. Although the authors do not make this point, explicit formalization and verification of this nonfunctional requirement would be a valuable endeavor. In particular, this would plausibly involve traces of operations at different levels of abstraction, while remaining amenable to calculational reasoning in an appropriate flavor of Kleene algebra. The authors do point out that tool support for converting the more strongly typed language of AoP into the still quite different language of Alloy is urgently needed. For some already-existing tool support for calculational reasoning, the interested reader may want to look at Mu et al.’s “Algebra of Programming in Agda” [2].

This well-written paper demonstrates how relational thinking and calculational proof are essential tools for rigorous software specification and development.

Beyond its technical merits, I consider its key contributions to be the sketching of a mindset and skill set for development by refinement that software developers can aspire to (and schools can educate for), and a nice use case for the tool support of the future.