Specification and Refinement of Databases and Transactions

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.