Abstract
The model-oriented formal method called VDM contains a specification language called VDM-SL. This language existed in a number of different dialects, but now a standard for the language has been prepared, including a dynamic semantics defined from a model-theoretic point of view. Thus, it is not at all clear that the defined semantics is appropriate for deriving proof rules which reflect the semantics. This paper focus on the possible ways of defining proof rules which reflect the semantics of explicit definitions which contain looseness.
The model-theoretic view which has been chosen for the definition of the semantics for VDM-SL, incorporates looseness by denoting the semantics of a (loose) specification as a set of models. The proof system should be designed such that properties which can be proved about a given specification should hold for all its models. This paper shows why it is an interesting challenge to develop a proof system which are able to do this.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Juan Bicarregui, John Fitzgerald, Peter Lindsay, Richard Moore and Brian Ritchie. Proof in VDM: A Practitioner’s Guide. Springer-Verlag, December 1993.
Hans Bruun, Flemming Dannn and Bo Stig Hansen. An Approach to the Static Semantics of VDM-SL. In VDM ‘81: Formal Software Development Methods, VDM Europe, Springer-Verlag, October 1991.
Edsger W. Dijkstra, Carel S. Scholten. Predicate Calculus and Program Semantics, chapter 4, pages 21–29. Springer-Verlag, 1990.
John Fitzgerald and Richard Moore. Experiences in Developing a Proof Theory for VDM Specifications. In Proceedings of the International Workshop on Semantics of Specification Languages,Utrect, October 1993, Springer Verlag, 1994. 17 pages.
John Fitzgerald. Private Communication. March 1993.
Ian Hayes. Private Communication. June 1993.
Cliff Jones, Kevin Jones, Peter Linsay and Richard Moore, editors. mural: A Formal Development Support System. Springer-Verlag, 1991. 421 pages.
Ralf Kneuper. Symbolic Execution as a Tool for Validation of Specifications. PhD thesis, Department of Computer Science, Univeristy of Manchester, 1989. 154 pages. Technical Report Series UMCS–89–7–1.
Peter Gorm Larsen, Michael Meincke Arentoft, Brian Monahan and Stephen Bear. Towards a Formal Semantics of The BSI/VDM Specification Language. In Ritter, editor, Information Processing 89, pages 95–100, IFIP, North-Holland, 1989.
Peter Gorm Larsen and Poul Bogh Lassen. An Executable Subset of Meta-IV with Loose Specification. In VDM ‘81: Formal Software Development Methods, VDM Europe, Springer-Verlag, October 1991.
Peter Gorm Larsen. The Dynamic Semantics of the VDM Specification Language. Technical Report, The Institute of Applied Computer Science, July 1992. 177 pages.
Poul Bogh Lassen, Kees de Bruin and Peter Gorm Larsen. The Dynamic Semantics of IFAD VDM-SL. June 1993. Internal document (IFAD)
Poul Bogh Lassen. IFAD VDM-SL Toolbox. In J.C.P. Woodcock and P.G. Larsen, editors, FME’93: Industrial-Strength Formal Methods, page 681, Springer-Verlag, Berlin Heidelberg, April 1993. 1 page.
Kees Middelburg. Syntax and Semantics of VVSL — A Language for Structured VDM Specifications. PhD thesis, University of Amsterdam, 1989. 395 pages.
Chris George and Soren Prehn. The RAISE Justification Handbook. The BCS Practitioners Series To be published by Prentice-Hall, 1994. 205 pages.
Morten Wieth. Loose Specification and its Semantics. In G.X. Ritter, editor, Information Processing 89, pages 1115–1120, IFIP, North-Holland, August 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this paper
Cite this paper
Larsen, P.G. (1994). Towards Proof Rules for Looseness in Explicit Definitions from VDM-SL. In: Andrews, D.J., Groote, J.F., Middelburg, C.A. (eds) Semantics of Specification Languages (SoSL). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3229-5_7
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3229-5_7
Publisher Name: Springer, London
Print ISBN: 978-3-540-19854-3
Online ISBN: 978-1-4471-3229-5
eBook Packages: Springer Book Archive