Abstract
A capsule view is given of the VDM Specification Language and the associated Specification Techniques for defining software, respectively the Systematic Derivation Techniques for Synthesizing & Proving correct Program Realizations from such, abstract Software Architectures.
The paper exhibits examples illustrating abstract syntax specifications of both abstract and derived concrete syntactic- and semantic domains, and denotational & derived operational elaboration function definitions mapping syntactic domain objects into their semantic domain object denotations, respectively into operations on these. In deriving the concrete programs from the abstract definitions, and in proving correctness, extensive use is made of invariant (-preserving) static- and dynamic well-formedness predicates and retrieval (or: abstraction) functions bringing concrete, realization-oriented objects ‘back’ into their defining abstract objects. Such uses are likewise illustrated. Examples of proofs based on the idea of commuting diagrams follows. These make use of a number of data structure lemmas: properties of the abstract and concrete objects chosen to represent, respectively realize, the specified software concepts. We finally exemplify the beginnings of such a catalogue of auxiliary lemmas.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
D.Bjørner: "META-IV: A Formal Meta-Language for Abstract Software Specifications", Technical Report, No. ID670, Dept. of Comp.Sci., Techn.Univ.of Denmark, November 1976, 45 pages.
—: "Programming Languages: Formal Development of Interpreters and Compilers", European ACM International Computing Symposium, ICS/77, North-Holland Publ., Proceedings, pp. 1–21, April 1977.
— and C.B.Jones: "The Vienna Development Method: The Meta-language", Springer-Verlag, Lecture Notes in Computer Science, vol.61, May 1978.
—: "Programming in the Meta-language, A Tutorial", in: [Bjørner 78a], pp. 24–217.
—: "Software Abstraction Principles: Tutorial Examples of An Operating System Command Language Specification and a PL/I-like ON-Condition Language Definition", in: [Bjørner 78a], pp. 337–374.
R.M.Burstall and J.Darlington: "Some Transformations for Developing Recursive Programs", Proc. 1975 Int'l. Conf. on Reliable Software, Los Angeles, pp. 465–472, to appear in JACM.
J. Darlington and R.M. Burstall: "A System which Automatically Improves Programs", Acta Informatica, vol.6, pp. 41–60, 1976.
S.Greibach: "Theory of Program Structures: Semantics, Schemes and Verification", Springer-Verlag, Lecture Notes in Computer Science, vol.36, 1975.
C.A.R. Hoare: "Proof of Correctness of Data Representations", Acta Informatica, vol.1, pp. 271–281, 1972.
C.B.Jones: "Program Specification and Formal Development", European ACM International Computing Symposium, ICS/77, North-Holland Publ., Proc., pp.537–553, 1977.
C.B.Jones: "The Meta-Language: A Reference Manual", in Bjørner 78a, pp. 218–277, 1978.
— and W.Henhapl: "A Formal Definition of ALGOL 60 as Described in the 1975 Modified Report", in: Bjørner 78a, pp. 305–336, 1978.
—: Program Development using Data Abstraction", to appear in Acta Informatica, 1978.
B. Liskov and S.N. Zilles: "Programming with Abstract Data Types", Proc.ACM Conf.on ‘Very High Level Languages', SIGPLAN Notices, vol.9,no.4,pp.50–59, 1974.
—: "Specification Techniques for Data Abstractions", IEEE Trans.on Software Eng., vol.SE-1,no.1, pp.7–19, 1975.
P. Lucas and K. Walk: "On the Formal Definition of PL/I", Ann.Rev.in Automatic Programming, Pergamon Press, vol.6,pt.3, pp.105–152, 1969.
J. McCarthy and J. Painter: "The Correctness of a Compiler for Arithmetic Expressions", Proc.Amer.Math.Soc., ‘Math.Aspects of Comp.Sci.', Proc.Symp.Appl.Math., vol.19, pp.33–41, 1967.
Z.Manna: "Introduction to the Mathematical Theory of Computation", McGraw-Hill, 1974.
R. Milner: "A Formal Notion of Simulation Between Programs", Memo 14, Computers and Logic Research Group, Univ.College, Swansea, UK., 1970.
—: "Program Simulation: An Extended Formal Notion", Memo 15, ibid, 1971.
—: "An Algebraic Definition of Simulation Between Programs", Stanford Comp.Sci.Dept. Rept.No. CS-205, 1971.
— and R.Weyhrauch: "Compiler Correctness in a Mechanized Logic", in: ‘Machine Intelligence', Ed. D.Michie, Edinburgh Univ.Press, vol.7, 1972.
F.L.Morris: "Advice on Structuring Compilers and Proving them Correct", Proc.ACM Symp.on ‘Principles of Programming Languages', Boston, Mass., Oct. 1973.
H.Bekić, D.Bjørner, W.Henhapl, C.B.Jones and P.Lucas: "A Formal Definition of a PL/I Subset", IBM Vienna Laboratory Techn.Rept., TR25.139, Dec.1974.
D. Bjørner: "Programming Languages: Linguistics and Semantics", European ACM International Computing Symposium, ICS/77, North-Holland Publ., Proceedings, pp. 511–526, 1977.
—: "Experiments in Block-structured GOTO Language Modeling: EXITs versis CONTINUATIONs", Techn. Rept., Comp.Sci.Dept., ID716, Techn.Univ. of Denmark, 1977.
—: "The Systematic Development of a Compiling Algorithm", Proceedings: 'state of the Art and Future Trends in Compilation', IRIA, Rocquencourt, France, 1978.
—: "Data Structure Diagrams: A Semantic Analysis of Network Data Base Concepts", presented at the IFIP WG2.2 Kyoto, Aug.1978 meeting (Techn.Rept., Comp. Sci.Dept., ID782, Techn.Univ.of Denmark).
C.B.Jones: "Formal Definition in Compiler Development", IBM Vienna Lab. Techn.Rept. TR25.145, Feb. 1976.
—: "Formal Definition in Program Development", Springer-Verlag Lecture Notes in Computer Science, vol. 23, pp. 387–443, 1975.
—: "Denotational Semantics of GOTO: An Exit Formulation and its Relation to Continuations", in: [Bjørner 78a], pp. 278–304. 1978.
—: "The Vienna Development Method: Examples of of Compiler Development", Proceedings: 'state of the Art and Future Trends in Compilation', IRIA, Rocquencourt, France, 1978.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1979 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bjørner, D. (1979). The vienna development method (VDM). In: Blum, E.K., Paul, M., Takasu, S. (eds) Mathematical Studies of Information Processing. Lecture Notes in Computer Science, vol 75. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09541-1_33
Download citation
DOI: https://doi.org/10.1007/3-540-09541-1_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09541-5
Online ISBN: 978-3-540-35010-1
eBook Packages: Springer Book Archive