Abstract
The PA (‘proof assistant’) has been instantiated with a hierarchy of theories with rules for VDM. These cover rules for inferring the well-definedness and the dynamic properties of VDM specifications. This chapter contains two case studies highlighting some of the capabilities of this special instantiation of the mural system. To prepare for the case studies, we first give a description of VDM specifications, and then describe how a few VDM constructs can be transformed into mural.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer-Verlag London Limited
About this chapter
Cite this chapter
Jones, C.B., Jones, K.D., Lindsay, P.A., Moore, R.D. (1991). Case Studies. In: mural: A Formal Development Support System. Springer, London. https://doi.org/10.1007/978-1-4471-3180-9_10
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3180-9_10
Publisher Name: Springer, London
Print ISBN: 978-3-540-19651-8
Online ISBN: 978-1-4471-3180-9
eBook Packages: Springer Book Archive