On the derivation of executable database programs from formal specifications

  • Thomas Günther
  • Klaus-Dieter Schewe
  • Ingrid Wetzel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 670)


Achieving wide acceptance of formal methods in software development requires a smooth integration with requirements analysis, design and implementation. Especially for database application systems there exist well-known approaches to conceptual modeling as well as a sophisticated implementation technology on the basis of database programming languagues. The work described in this paper is based on a scenario, where the B method is coupled with a conceptual modeling language TDL and a database programming language DBPL. Both these languages can be represented in B. We concentrate on the problem of characterizing those B specifications that are sufficiently refined in order to be transformed into equivalent DBPL programs. This gives rise to some kind of implementability proof obligation.

Moreover, we show that the transformation itself can be regarded as a term rewriting task based on a representation by term algebras of the languages involved. For this task we exploit order-sorted algebra by using the OBJ system.


Formal Method Proof Obligation Record Type Abstract Machine Final Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. R. Abrial: A Formal Approach to Large Software Construction, in J.L.A. van de Snepscheut (Ed.): Mathematics of Program Construction, Proc. Int. Conf. Groningen, The Netherlands, June 89, Springer LNCS 375, 1989Google Scholar
  2. 2.
    A. Borgida, J. Mylopoulos, J. W. Schmidt, I. Wetzel: Support for Data-Intensive Applications: Conceptual Design and Software Development, Proc. of the 2nd Workshop on Database Programming Languages, Salishan Lodge, Oregon, June 1989Google Scholar
  3. 3.
    E. W. Dijkstra, C. S. Scholten: Predicate Calculus and Program Semantics, Springer-Verlag, 1989Google Scholar
  4. 4.
    J. A. Goguen, T. Winkler: Introducing OBJ3, SRI International, Technical Report, August 1988Google Scholar
  5. 5.
    T. Günther: Charakterisierung und Transformation in DBPL implementierbarer Abstrakter Maschinen (in German), Master Thesis, University of Hamburg, August 1992Google Scholar
  6. 6.
    R. Hull, R. King: Semantic Database Modeling: Survey, Applications and Research Issues, ACM Computing Surveys, vol. 19(3), September 1987Google Scholar
  7. 7.
    M. Jarke, J. Mylopoulos, J. W. Schmidt. Y. Vassiliou: DAIDA: An Environment for Evolving Information Systems, ACM ToIS, vol. 10 (1), January 1992, pp. 1–50CrossRefGoogle Scholar
  8. 8.
    C. B. Jones: Systematic Software Development using VDM, Prentice-Hall International, London 1986Google Scholar
  9. 9.
    F. Matthes, J. W. Schmidt: DBPL Rationale and Report, FIDE technical report, 1992Google Scholar
  10. 10.
    J. Mylopoulos, P. A. Bernstein, H. K. T. Wong: A Language Facility for Designing Interactive Database-Intensive Applications, ACM ToDS, vol. 5 (2), April 1980, pp. 185–207CrossRefGoogle Scholar
  11. 11.
    G. Nelson: A Generalization of Dijkstra's Calculus, ACM TOPLAS, vol. 11 (4), October 1989, pp. 517–561CrossRefGoogle Scholar
  12. 12.
    K.-D. Schewe, J. W. Schmidt, I. Wetzel, N. Bidoit, D. Castelli, C. Meghini: Abstract Machines Revisited, FIDE technical report 1991/11Google Scholar
  13. 13.
    K.-D. Schewe, J. W. Schmidt, I. Wetzel: Specification and Refinement in an Integrated Database Application Environment, in S. Prehn, H. Toetenel (Eds.): Proc. VDM 91, Noordwijkerhout, October 1991, Springer LNCSGoogle Scholar
  14. 14.
    J. M. Spivey: Understanding Z, A Specification language and its Formal Semantics, Cambridge University Press, 1988Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Thomas Günther
    • 1
  • Klaus-Dieter Schewe
    • 1
  • Ingrid Wetzel
    • 1
  1. 1.Dept. of Computer ScienceUniversity of HamburgHamburg 54FRG

Personalised recommendations