A practical approach to software engineering using Z and the refinement calculus

ABSTRACT

We present a methodology for the formal specification and development of software systems using Z and the refinement calculus. The methodology combines the data structuring capabilities and the codified discrete mathematics of Z with the data encapsulation properties and development style of the refinement calculus, and it aims to provide a formal path from design to implementation without unnecessary transformations of notation or the definition of a new calculus. It is illustrated here by the development of two systems, a simply diary and (part of)a text editor, and is contrasted with the use of Z on its own. We discuss related and future work and conclude with some general comments on applied formal methods.

REFERENCES

• 1: GEOFF BARRETT, Formal methods applzed to a Jioating point number system, Technical Monograph PRG-58, Programming Research Group, Oxford University Computing Laboratory, January 1987.
• 2: Antoni Diller, Z: An Introduction to Formal Methods, John Wiley & Sons, Inc., New York, NY, 1990
• 3: IAN HAYES, Applying formal specification to soflware development tn industry, IEEE 'llansactions on Software Engineering, SE-11 (1985), pp. 169- 178.
• 4: Ian Hayes , C. B. Jones, Specifications are not (necessarily) executable, Software Engineering Journal, v.4 n.6, p.330-338, Nov. 1989
• 5: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 6: M.H. JARVIS, C.C. MORGAN, AND P.H.B. GARDINER, The Red manual, internal report, Programming Research Group, Oxford University Computing Laboratory, 1991.
• 7: C B Jones, Systematic software development using VDM, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1986
• 8: G. JONES, Programming tn Occam, Prentice- Hall, 1987.
• 9: Steve King, Z and the Refinement Calculus, Proceedings of the Third International Symposium of VDM Europe on VDM and Z - Formal Methods in Software Development, p.164-188, April 17-21, 1990
• 10: The use of Z at IBM hursley: Experiences and ;esults, internal report, Programming Research Group, Oxford University Computing Laboratory, October 1991. To appear in Ian Hayes (Ed.), Specification Case Studzes, %d Edition, Prentice-Hall.
• 11: Carroll Morgan, The specification statement, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.403-419, July 1988 [doi>10.1145/44501.44503]
• 12: Carroll Morgan, Programming from specifications, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 13: DAVID S. NEILSON. From Z to C: dlushation ot a rtgorous development method. D .Phil. thesis, Oxford University, 1991.
• 14: J.E. NICHOLLS AND S.M. BRIEN (EDs), Z base standard, Technical Report ZIP/PRG/92/121, ZIP Project, Oxford University Computing Laboratory, 1993.
• 15: U.K. MINISTRY OF DEFENCE, The procurement of safety crttical software in defence equipment. Interim Defence Standard 00-55, Issue 1, April 1991.
• 16: J. M. Spivey, The Z notation: a reference manual, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 17: B.A. SUFRIN, Formal speczficataon of a displayoriented text editor, Science of Computer Programming, 1 (1982), pp. 157-202.
• 18: KENNETH R. WOOD, The elusive software rejinery: A case study in program development, in 4th Refinement Workshop, Joseph M. Morris and Roger C. Shaw, eds., BCS Workshops in Computing, Springer-Verlag, 1991, pp. 281-325.
• 19: -. Parallel Logic Simulation and Applied Formal Methods. D .Phil. thesis, Oxford University, 1992.
• 20: - Composmg specajcations an the refinement' calculus, Technical Report, Programming Research Group, Oxford University Computing Laboratory, 1993 (in preparation).
• 21: Kenneth R. Wood, A pragmatic basis for the formal development of distributed systems, Proceedings of the 7th international workshop on Software specification and design, December 06-07, 1993, Redondo Beach, California

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

          Nouns: Z

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.10 Design**
            Subjects: Methodologies**

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.3 Software Management
          Subjects: Software development

General Terms:
Design, Management, Theory