SQRL Report No. 15
Software Quality Research Laboratory
Department of Computing and Software
Parnas together with a number of colleagues established the systematic use of certain kinds of tables as a useful tool in software documentation and inspection with an accessible, multi-dimensional syntax and intuitive semantics.
Previous approaches to formalisation of table semantics based their definitions on the multi-dimensional array structure of tables and thus achieved close correspondence with the intuitive understanding of tables.
In this paper, we argue that a different view, supporting a compositional semantics, is more advantageous for tool support and for reasoning about tables. For this purpose, we also need a compositional table syntax, and we perform an analysis of table syntax that leads us to a particular compositional view of table structure.
This simple, inductive view of the structure of tables allows us to provide highly flexible tools for defining the semantics of tabular expressions. The straight-forward compositional formalisation of table semantics on the one hand yields very general table transformation theorems and enables us to perform fully formal proofs for these theorems in a mechanised theorem prover, and on the other hand also may serve as basis for the implementation of semantics-aware table support tools.