Geert B. Clemmensen
ABSTRACT
The Vienna Development Method (VDM) has been employed by Dansk Datamatik Center (DDC) on a large-scale, industrial Ada compiler development project. VDM is a formal specification and development method in that it insists on the initial specifications and all design steps being expressed in a formal (mathematically based) notation.
This paper gives an overview of how VDM was used in the various steps of the DDC Ada project, and we guide the reader through the steps involved from the initial formal specification of Ada down to the actually coded multipass compiler. Finally we report on the quantitative and qualitative experiences we have gained, both as regards the technical suitability of VDM for the project and as regards the implications on software management and quality assurance.
- 1.H. Beki@@@@, D. Bjørner, W. Henhapl, C.B. Jones and P. Lucas: A Formal Definition of a PL/I Subset, IBM Vienna, TR25.139, Dec. 1974.Google Scholar
- 2.D. Bjørner, O.N. Oest (eds.): Towards a Formal Description of Ada, Lecture Notes in Computer science, Vol. 98, Springer Verlag, 1980. Google ScholarDigital Library
- 3.D. Bjørner, C.B. Jones: Formal Specification and Software Development, Prentice-Hall International Series in Computer Science, 1982.Google Scholar
- 4.A. Church: The Calculi of Lambda-Conversion, Annals of Math. Studies, 6, Princeton University Press, N.J., 1941. Google ScholarDigital Library
- 5.B. Cohen, M.I. Jackson: A Critical Appraisal of Formal Software Development Theories, Methods and Tools, ESPRIT preparatory study, STL, June 1983.Google Scholar
- 6.L. Ibsen, L.O.K. Nielsen, N.M. Jørgensen: A-Machine Specification, ADA/RFM/0001, Christian Rovsing A/S, March 1983.Google Scholar
- 7.V. Donzeau-Gouge, G. Kahn, B. Lang, B. Krieg-Brueckner: On the Formal Definition of Ada, Rivista Di Informatica, Vol. X, N.1, January-March 1980.Google ScholarCross Ref
- 8.G.B. Clemmensen, H.H. Løvengreen: Portable Ada Programming System, Dynamic Semantics, Description of Ada Tasking, DDC, Nov. 1981.Google Scholar
- 9.J. Jørgensen: Portable Ada Programming System, Ada Static Semantics, AS1 → AS2 Transformation, DDC, Feb. 1982.Google Scholar
- 10.H. Bruun, J. Bundgaard, J. Jørgensen: Portable Ada Programming System, Ada Static Semantics, Well-formedness Criteria, DDC, March 1982.Google Scholar
- 11.J.S. Pedersen, P. Folkjaer, I.ø. Hansen: Portable Ada Programming System, Dynamic Semantics, Description of Sequential Ada, DDC, March 1982.Google Scholar
- 12.S. Prehn, I.ø. Hansen, S.U. Palm, P. Gøbel: Formal Methods Appraisal, Part II, A critical Examination of VDM, DDC, June 1983.Google Scholar
- 13.DIANA Reference Manual, Revision 3, TARTAN Laboratories INC, Febr. 1983.Google Scholar
- 14.Reference Manual for the Ada Programming Language, ANSI/MIL-STD 1815A, January 1983.Google Scholar
- 15.J.E. Stoy: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977. Google ScholarDigital Library
Index Terms
- Formal specification and development of an ada compiler - a vdm case study
Recommendations
Transformation of a semi-formal specification to VDM
KBSE'92: Proceedings of the 7th International Conference on Knowledge-Based Software EngineeringDescriptions of the requirements of a software system written in an unconstrained natural language are considered to be informal. Informal descriptions are known to have the potential to contain ambiguities, partial descriptions, inconsistencies, ...
VDM and Z: A comparative case study
AbstractThe specification notations of VDM and Z are closely related. They both use model-based specification techniques and share a large part of their mathematical notation. However, the approaches taken to writing specifications differ in other, more ...
Comments