Abstract
This chapter presents the Vienna Development Method, which is one of the older formal specification languages. It was developed at the IBM laboratory in Vienna as a method to specify the semantics of the PL/1 programming language, and it evolved into a formal specification language with a rigorous software development method with rules to verify the steps of development. The rules enable the executable specification, i.e. the detailed code, to be obtained from the initial specification via refinement steps, such that the executable code is a valid implementation of the formal specification.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Meta IV was a pun on metaphor.
- 2.
The IFAD Toolbox has been renamed to VDMTools (as IFAD sold the VDM Tools to CSK in Japan).
- 3.
f † g is the VDM notation for function override. The notation f ⊕ g is employed in Z .
- 4.
The problem with 3-valued logic is that they are less intuitive than classical 2-valued logic.
References
D. Bjørner, C. Jones, Formal Specification and Software Development. Prentice Hall International Series in Computer Science (1982)
M.M.A. Airchinnigh, Computation Models and Computing. Ph.D. thesis, Dept. of Computer Science. Trinity College Dublin
D. Andrews, D. Ince, Practical Formal Methods with VDM (McGraw Hill International, 1991)
C. Jones, Systematic Software Development Using VDM (Prentice Hall International, 1986)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
O’Regan, G. (2017). Vienna Development Method. In: Concise Guide to Formal Methods. Undergraduate Topics in Computer Science. Springer, Cham. https://doi.org/10.1007/978-3-319-64021-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-64021-1_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-64020-4
Online ISBN: 978-3-319-64021-1
eBook Packages: Computer ScienceComputer Science (R0)