Abstract
The variants of specification languages used with the Vienna Development Method (VDM) offer a rather expressive notion of types. Higher order function types, recursively defined types, and a notion of union types which does not require injection and projection are all included, not to mention subtypes characterized by arbitrary predicates.
Besides this, VDM specifications are in general not executable so dynamic type checking does not make sense. However, proof of their total consistency (satisfiability), as advocated by Cliff Jones [5], covers all type checking including what is usually considered “dynamic”, e.g. index range checks. In addition, it ensures other desirable properties such as termination of recursively defined functions.
In this paper, we identify a number of general problems concerning automatic type checking of VDM specifications and the relation to consistency proofs. The authors are currently investigating different ways of handling the problems and the presentation includes outlines of some of these.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Robert M. Amadio and Luca Cardelli. Subtyping recursive types. Research Report 62, Systems Research Center, Digital Equipment Corporation, 1990.
Dines Bjørner and Cliff B. Jones, editors. The Vienna Development Method: The Meta-Language, volume 61 of Lecture Notes in Computer Science. Springer-Verlag, 1978.
Robert S. Boyer and J. Strother Moore. A Computational Logic Handbook, volume 23 of Perspective in Computing. Academic Press, Inc., 1988.
Hans Bruun, Bo Stig Hansen, and Flemming Damm. An approach to the static semantics of VDM-SL. This volume.
Cliff B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 2. edition, 1990.
Peter Gorm Larsen. The dynamic semantics of the BSI/VDM specification language. Draft version, August 1990.
Robert Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.
B. Monahan and A. Walsh. Context conditions for the STC VDM reference language. Technical Report 725 05308 ed. 2, STC pic/Manchester University, 1986.
Nico Plat, Ronald Hiujsman, Jan van Katwijk, Gertjan van Oosten, Kees Pronk, and Hans Toetenel. Type checking BSI/VDM-SL. In VDM '90, VDM and Z—Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 399–425. VDM-Europe, Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, F., Hansen, B.S., Bruun, H. (1991). On type checking in VDM and related consistency issues. In: Prehn, S., Toetenel, W.J. (eds) VDM'91 Formal Software Development Methods. VDM 1991. Lecture Notes in Computer Science, vol 551. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54834-3_6
Download citation
DOI: https://doi.org/10.1007/3-540-54834-3_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54834-8
Online ISBN: 978-3-540-46449-5
eBook Packages: Springer Book Archive