Specification and Refinement of Databases and Transactions

Abstract

The development process of data-intensive information systems passes through several stages from requirements modeling through conceptual design down to implementation. In DAIDA we used the language TDL for design specification and DBPL, a procedural database programming language with persistent values and transactions, for implementation. In focusing on the transformation from TDL to DBPL we discuss the relationship between the specification and various refinement steps that lead to efficient database programs. As a framework for transformations we use Abrial’ s Abstract Machine formalism. TDL-designs can be mapped into Abstract Machines, which are then the subject of refinement. The complete reification of TDL designs is illustrated by an example.

The Abstract Machine approach is based on the encapsulation of state descriptions by variables and invariants as well as on state transitions expressed in Dijkstra’s substitution calculus. This sets up the formal basis of the mapping assistant. The relationship between the predicative and the substitution-based specification style is discussed formally using predicate transformers and set-theoretic semantics. We state an equivalence between predicative specifications used by TDL transactions and Dijkstra’s substitutions and discuss operational and data refinement in predicative and in substitution-based specifications.

We would like to thank J. R. Abrial and our colleagues in DAIDA, especially the researchers at BP research centre, for many fruitful discussions and comments. We also want to thank Paul Gardiner from the Programming Research Group at Oxford University for interesting discussions and his contribution to the set-theoretic semantics of substitutions. Furthermore we thank Michael Mertikas for his contribution to earlier versions of this paper.