The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. The the software can be developed smoothly in the same frame. The combination of COOZ and refinement calculus can build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implementation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
de Bakker J Wet al. (eds.) InProc. REX Workshop on Stepwise Refinement on Distributed Systems, Lecture Notes in Computer Science 430, Springer-Verlag, 1989.
Hoare C A R, He J. The Weakest Prespecification.Fund. Inform. IX 1986, pp.51–84.
Jones C B, Shaw R C, Denvir T (eds.). In5th Refinement Workshop in Computing, Springer-Verlag, 1992.
Back R J R. On the correctness of refinement in program development [dissertation]. Report A-1978-4. Department of Computer Science, University of Helsinki, 1978.
Morris J M. A theoretical basis of stepwise refinement and programming calculus.Science of Computer Programming, 1987, 9(2): 287–306.
Morgan C C. The specification statement.ACM Transaction on Programming Language and Systems, July 1988, 10(3): 403–419.
Back R J R, von Wright J. Refinement calculus, Part I: Sequential programs. InREX Workshop for Refinement of Distributed Systems, Lecture Notes in Computer Science 430, Nijmegen, The Netherlands, Springer-Verlag, 1989.
Gardiner P H B, Morgan C. A single complete rule for data refinement.Formal Aspects of Computing, 1993, 5(4): 367–382.
Spivey J M. The Z Notation: A Reference Manual. Prentice-Hall, International Series in Computer Science, 2nd Edition, 1992.
Stepeney Set al. More powerful Z data refinement. InZUM’98: The Z Formal Specification Notation, 11th International Conference of Z Users, Bowen J P, Hinchey M G (eds.), September 1998, Proceedings, Lecture Notes in Computer Science 1493, Springer-Verlag, 1998.
Nellson D S. From Z to C: Illustration of a rigorous development method [dissertation]. PRG-79, Oxford University, Computing Laboratory, February, 1990.
King S. Z and the refinement calculus. In VDM and Z — Formal Methods in Software Development, Bjørner Det al. (eds.), Lecture Notes in Computer Science 428, VDM-Europe, Springer-Verlag, 1990, pp. 164–188. Also published as a Technical Monograph PRG-79, Oxford University, Computing Laboratory, February, 1990.
Morgan C C. Programming from Specifications. Prentice-Hall, International Series in Computer Science, 2nd Edition, 1994.
Yuan Xiaodong, Hu Deqiang, Xu Haoet al. COOZ: A complete object-oriented extension to Z.ACM Software Engineering Notes, 1998, 23(4): 78–81.
Gardiner P H B, Morgan C. Data refinement of predicate transformers.Theoretical Computer Science, 1991, 87: 143–162.
J. von Wright. A lattice-theoretical base for program refinement [dissertation]. Abo Akademi University, SF-20500 Turku, Finland, Sept., 1990.
Rimvydas Ruksenas. A tool for data refinement. Technical Report, TUCS — Turku Centre for Computer Science, Number TUCS-TR-119, August, 1997.
The work is supported by the National Natural Science Foundation of China (No.69673006) and the National Ninth Five-Year Project (98-780-01-07-06) of China.
WANG Yunfeng received his Ph.D. degree from Department of Computer Science and Technology, Nanjing UIniversity in 2000. He is now working in Meteorology College, PLA University of Science and Technology. His research interests include formal methods and object-oriented technology.
PANG Jun received his M.S. degree from Department of Computer Science and Technology, Nanjing University in 2000. He is now a Ph.D. candidate in Department of Software Engineering, National Center for Mathematics and Computer Science (CWI), Netherlands. His interests include process algebra, protocol verification, Z & refinement calculus and object-oriented technology.
YANG Zhaohui received his B.S. degree from Department of Computer Science and Technology at Nanjing University in 2000. He is now an M.S. candidate of Department of Computer Science and Technology, Nanjing University.
ZHENG Guoliang is a professor in Department of Computer Science and Technology, Nanjing University. He received his B.S. degree in computer science from Nanjing University in 1961. His main research area is software engineering.
About this article
Cite this article
Wang, Y., Pang, J., Zha, M. et al. A formal software development approach using refinement calculus. J. Comput. Sci. & Technol. 16, 251–262 (2001). https://doi.org/10.1007/BF02943203
- formal development method
- refinement calculus
- formal specification