Abstract
Formal specification of software requirements has been recognised as an essential ingredient to improve the quality of delivered code. When integrated with the structuring mechanisms of object-orientation, formal specifications can provide a powerful tool for the software developer. However, the formal specification of particularly large systems needs to be supported by tools which assist the specifier or reader of the specification either to understand and/or to reason about a specification. The simplest form of reasoning is that of type checking. This paper develops a simple but useful set of rules for type checking the object-oriented formal specification language Object-Z. Although type checkers exist for Z, at present none exists for Object-Z. The lack of a type checker for Object-Z is a hinderence to a wider and more consistent use of this specification language as an integral component in developing high-quality software products.
Chapter PDF
Similar content being viewed by others
Keyword Codes
Keywords
References
Barden, R., Stepney, S. and Cooper, D., “The Use of Z”, in Proc. of 6th Z User Workshop, Nicholls, J.E. ( ed. ), Springer-Verlag, 1991, pages 99–124.
Carrington, D., Duke, D., Duke, R., King, P., Rose, G. and Smith, G., “Object-Z: An Object-oriented Extension to Z”, in Formal Description Techniques, II (FORTE’89), Vuong, S. ( ed. ), North-Holland, 1990, pages 281–296.
Chen, J. and Durnota, B., “Type Checking Object-Z Specifications”, in preparation.
Craigen, D., Gerhart, S. and Ralston, T., An International Survey of Industrial Applications of Formal Methods, two volumes, U.S. Department of Commerce, MD 20899, 1993.
Duke, R., King, P., Rose, G. and Smith, G., “The Object-Z Specification Language - Version 1”, Technical Report No. 91–1, Software Verification Research Centre, The University of Queensland, May 1991.
Reed, J.N. and Sinclair, J.E., “An Algorithm for Type-Checking Z”, Technical Monograph RG-81, Oxford University, 1990.
Rose, G., “Object-Z”, in Object Orientation in Z, Stepney, S., Barden, R. and Cooper, D. (eds.), Springer-Verlag, Chapter 6, 1992.
Spivey, J.M., The Z Notation: A Reference Manual, International Series in Computer Science, Prentice-Hall, 1989.
Weber-Wulff, D., “Selling Formal Methods to Industry”, in Proc. of FME93: Industrial-Strength Formal Methods, Woodcock, J.C.P. and Larsen, P.G. (eds.), LNCS 670, Springer-Verlag, 1993, pages 671–678.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Chen, J., Dumota, B. (1995). Type Checking Classes in Object-Z to Promote Quality of Specifications. In: Lee, M., Barta, BZ., Juliff, P. (eds) Software Quality and Productivity. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34848-3_15
Download citation
DOI: https://doi.org/10.1007/978-0-387-34848-3_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6544-1
Online ISBN: 978-0-387-34848-3
eBook Packages: Springer Book Archive