The stepwise development of software development graphs — Meta-programming VDM developments

An extended abstract
  • Dines Bjørner
Development Methods
Part of the Lecture Notes in Computer Science book series (LNCS, volume 252)


In VDM development of software proceeds from specification, via stages of design, to coding. A classical way of illustrating this is by the "waterfall- diagram" of fig.3.

As a planning aid, drawing such simple sequences of boxes as shown in fig. 3. really is of no help. In this paper we shall carefully develop an example, so-called software development graph. Thus from a graph like fig. 3. we shall arrive at a graph like that of fig. 9, which is claimed far more useful.

The meaning of nodes (boxes or vertices) and edges (arrows or arcs) is given relative to VDM, and in four different versions: one each for theoretical computer science, programming methodology, software engineering and management.

Our basic point is the following (see fig. 4.): before actually developing the various components (formulas) of the specifications (nodes s ), before actually developing the design ( dl ) from the specification ( s ), or more concrete design ( d2 ) from more abstract design ( dl ), and before actually developing the various components (formulas) of the designs (see figs. 7-8), etc., we meta-develop the development, that is we decide on a development strategy, we specify which design choices to make (ie. the basic object and operation transformation ideas), and we specify which components our specifications and designs will then consists of.

Our derived point is then the following: even the development of the final, so-called consistent & complete software development graph, will take place as a stepwise development, from that almost meaninglessly expressed by fig. 3, via those of the more and more detailed figs. 4-5-6-7-8, to fig. 9!

The paper is discursive. An appendix will show some of the actual formulas whose construction are being planned by the software meta-development method of this paper.


Abstract Syntax Denotational Semantic Dynamic Semantic Entire Graph Software Development Project 
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.

Copyright information

© Springer-Verlag Berlin Heidelberg 1987

Authors and Affiliations

  • Dines Bjørner
    • 1
    • 2
  1. 1.Department of Computing ScienceTechnical University of DenmarkLyngbyDenmark
  2. 2.Dansk Datamatik Center Lundtoftevej 1CLyngbyDenmark

Personalised recommendations