We present a framework for the development of information systems based on the premise that the knowledge that influences the development process needs to somehow be captured, represented and managed if the development process is to be rationalized. Experiences with a prototype environment developed in ESPRIT project DAIDA demonstrate the approach. Specifically, the project has implemented an environment based on state-of-the-art languages for requirements modelling, design and implementation of information systems. In addition, the environment offers tools for aiding the mapping process from requirements to design and then to implementation, also for representing decisions reached during the development process. The development process itself is represented explicitly within the system, thus making the DAIDA development framework easier to comprehend, use and modify.

This document explains the installation and use of the P-Quest system (version 14) on Sun-4 hardware platforms.

P-Quest was developed at the University of Hamburg, Germany, and adds orthogonal persistence to the programming language Quest developed by Luca Cardelli at DEC SRC, Palo Alto, USA. The implementation of P-Quest was carried out in the ESPRIT-II basic research project FIDE and utilizes the Napier persistent object store provided by the University of St. Andrews, Scotland.

This document describes how to compile, link and execute Modula-2 programs on a VAX under the VMS operating system. The VAX Modula-2 Compiler is based on an implementation of Modula-2 for the PDP-11 developed by a group under the direction of Prof. N. Wirth at the ETH Zürich.

This document also describes how to compile, link and execute DBPL programs on a VAX under the VMS operating system. DBPL is a relational database programming language that has Modula-2 as its algorithmic kernel. The DBPL Compiler is a fully upward compatible extension of the VAX Modula-2 Compiler.

The formalism of abstract machines has already been successfully used to establish a mapping from conceptual design modelled in the semantic data and transaction language TDL down to an implementation in the database programming language DBPL. We revise this formalism and compare it to predicative specifications as found in the formal specification language Z. The results show that the specification style of abstract machine operations, which is based on a slight extension of Dijkstra's substitution calculus, is in fact equivalent to the Z style. The main part of the paper addresses the problems of modularization, inheritance and refinement of abstract machines. We give formal definitions for the specialization and the refinement of substitutions and show their equivalence to the corresponding definitons in predicative specifications. We present some more partial results and conclude by mentioning some open problems.

The formal foundation of object-oriented databases is still an open problem. In this paper a formalization of kernel object-oriented design concepts is achieved by an automatizable transformation into a specification language with a clear mathematical semantics. This approach allows object-oriented design to be extensible.

The preservation of advantages of relational databases requires the definability of generic operations for the insertion, deletion and update of single objects. It is shown that such generic operations can only be defined for value-representable classes. The possibility to detect value-representability contributes to the safety for object-oriented design.

Database application programs may be considered as good candidates for the application of formal specification methods, because much of the database and transaction semantics can be captured in terms of integrity constraints as well as pre- and postconditions. Furthermore, the use of current transaction models as units of database state transitions favours the use of Dijkstra's substitutions.

Traditional DBMS solutions guarantee database integrity by expensive tests at transaction commit time. In the DAIDA project a different approach was taken interpreting database constraints as parts of formal specifications and by extracting correct database programs from such specifications. Database and transaction constraints are captured by an expressive semantic data model in the style of TAXIS, transformed into Abstract Machines and finally refined into AM versions that are equivalent to programs written in the strongly-typed database programming language DBPL.

The work reported in this paper evaluates the DAIDA experience and addresses the shortcomings of DAIDA. A new formal specification language SAMT is proposed that essentially allows to structure and modularize specifications and to capture particular classes of constraints by its type system. Moreover, SAMT is considered as a framework for both the specification of database applications as well as the refinement of specifications into executable programs, thus eliminating some of the complexity issues found in the multi-language approach of DAIDA.