Abstract
The work presented here concerns abstract specification of type checking for a specification language VDM-SL of the Vienna Development Method. Where previous work has focussed on rejection of “obviously” ill-typed specifications we do, in addition, consider acceptance of “obviously” well-typed expressions.
The presentation includes essential parts of the definition of several well-formedness predicates for increasingly advanced type analyses. In order to emphasize the similarities and symmetries, the different predicates are defined in terms of a single, parameterized predicate.
In other work, an independent definition of (type) consistency of VDM-SL specifications has been put forward. We discuss the necessary conditions for the correctness of our type checking with respect to this definition.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Samson Abramsky and Chris Hankin, editors. Abstract Interpretation of Declarative Languages. Ellis Horwood Series in Computers and Their Applications. Ellis Horwood Limited, 1987.
Marek Bednarczyk, Andrzej M. Borzyszkowski, and Wiesław Pawłowski. Towards the semantics of the definitional language of MetaSoft. In VDM '90, VDM and Z— Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 477–503. VDM-Europe, Springer-Verlag, 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.
Hans Bruun, Bo Stig Hansen, and Flemming Damm. An approach to the static semantics of VDM-SL. Technical Report 1991-90, Department of Computer Science, The Technical University of Denmark, 1991.
Flemming Damm, Bo Stig Hansen, and Hans Bruun. Type checking in VDM and related consistency issues. This volume.
Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. Technical report, School of Computer Science, Carnegie Mellon University, 1990.
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, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.
B. Monahan and A. Walsh. Context conditions for the STC VDM reference language. Technical Report 725 05308 ed. 2, STC plc/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.
Andrzej Tarlecki and Morten Wieth. A naive domain universe for VDM. In VDM '90, VDM and Z-Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 552–579. 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
Bruun, H., Hansen, B.S., Damm, F. (1991). An approach to the static semantics of VDM-SL. 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_15
Download citation
DOI: https://doi.org/10.1007/3-540-54834-3_15
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