Abstract
Large Z specifications require testing if they are to be at all credible and translation to Prolog provides one means of doing this. Experience with PiZA (Prolog Z Animator), a system designed to carry out this translation automatically, is described. The paper gives a brief description of the principles of the translation with some practical details of using PiZA. Experience in animating large specifications of about the size of a small compiler is discussed in terms of the performance, the problems presented by the form of the Prolog translation, the processing of input and output values and the use of diagnostics. The paper concludes with a discussion of the use of Z as a design language.
® British Crown Copyright 1996/DERA. Published with the permission of the controller of Her Britannic Majesty's Stationery Office.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Dick AJJ, Krause PJ, and Cozens J. Computer aided transformation of Z into Prolog. Workshops in Computing, pages 71–85. Springer-Verlag, 1990.
Jordan D, McDermid JA, and Toyn I. CADiZ — computer aided design in Z. Workshops in Computing, pages 93–104. Springer-Verlag, 1991.
Toyn I. CADiZ Quick Reference Guide. York Software Engineering Ltd, University of York, York YO1 5DD, UK, 1990.
Xiaoping J. ZTC: A Type Checker for the Z Notation. School of Computer Science, DePaul University, Chicago, Illinois, USA, 1995.
Spivey JM. The Fuzz Manual. Computing Science Consultancy, 2 Willow Close, Garsington, Oxford OX9 9AN, UK, 2nd edition, 1992.
Spivey JM. The Z Notation: A Reference Manual. Series in Computer Science. Prentice Hall International, 2nd edition, 1992.
Hewitt MA. Automated animation of Z using Prolog. B.S.c. Project Report, Department of Computing, Lancaster University, 1991.
Hewitt MA. Optimization of Prolog generated from Z specifications. Master's thesis, Department of Computing Science, University of Aberdeen, 1992. Available from http://www.noodles.demon.co.uk/PiZA/PiZAOldDocs.html.
West MM and Eaglestone BM. Software development: Two approaches to animation of Z specifications using Prolog. IEE/BCS Software Engineering Journal, 7(4):264–276, July 1992.
OSF. ANDF, application portability and open systems. Technical report, Open Software Foundation, 11 Cambridge Center, Cambridge, MA 02142, USA, 1991.
Knott RD and Krause PJ. The implementation of Z specifications using program transformation systems: The SuZan project. In C. Rattray and R. G. Clark, editors, The Unified Computation Laboratory, volume 35 of IMA Conference Series, pages 207–220, Oxford, UK, 1992. Clarendon Press.
TA Consultancy Services Ltd, ‘The Barbican’ East Street, Farnham, Surrey, UK, GU9 7TB. Intermediate Language Manual for MALPAS, 6th edition, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hewitt, M.A., O'Halloran, C.M., Sennett, C.T. (1997). Experiences with PiZA, an Animator for Z. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds) ZUM '97: The Z Formal Specification Notation. ZUM 1997. Lecture Notes in Computer Science, vol 1212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027282
Download citation
DOI: https://doi.org/10.1007/BFb0027282
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62717-3
Online ISBN: 978-3-540-68490-9
eBook Packages: Springer Book Archive