Relational algebra offers to software engineering the same degree of conciseness and calculational power as linear algebra in other engineering disciplines. Binary relations play the role of matrices with similar emphasis on multiplication and transposition. This matches with Alloy's lemma “everything is a relation” and with the relational basis of the Algebra of Programming (AoP). Altogether, it provides a simple and coherent approach to checking and calculating programs from abstract models. In this paper, we put Alloy and the Algebra of Programming together in a case study originating from the Verifiable File System mini-challenge put forward by Joshi and Holzmann: verifying the refinement of an abstract file store model into a journaled (Flash) data model catering to wear leveling and recovery from power loss. Our approach relies on diagrams to graphically express typed assertions. It interweaves model checking (in Alloy) with calculational proofs in a way which offers the best of both worlds. This provides ample evidence of the positive impact in software verification of Alloy's focus on relations, complemented by induction-free proofs about data structures such as stores and lists.

Several studies have shown how spreadsheets are pervasive in many organizations as a form of end-user programming. Despite their importance and long lifespan, they are seldom developed with maintenance concerns in mind, and organizations have no efficient way of estimating the risk they present. In this paper we take a first step towards automated assessment of spreadsheet maintainability. We use the Goal Question Metric approach to select metrics relevant for maintainability and apply the selected metrics to a spreadsheet corpus in order to study their behavior "in the wild". We observe that the majority of the metrics behave in the same way as similar ones for traditional software systems, which means that existing methodologies to assess maintainability can be applied to spreadsheets as well. This opens the possibility of creating instruments for organizations that rely on spreadsheets to start actively managing their maintainability.