Structuring Z specifications with views

ABSTRACT

A view is a partial specification of a program, consisting of a state space and a set of operations. A full specification is obtained by composing several views, linking them through their states (by asserting invariants across views) and through their operations (by defining external operations as combinations of operations from different views). By encouraging multiple representations of the program's state, view structuring lends clarity and terseness to the specification of operations. And by separating different aspects of functionality, it brings modularity at the grossest level of organization, so that specifications can accommodate change more gracefully. View structuring in Z is demonstrated with a few small examples. Both the features of Z that lend themselves to view structuring and those that are a hindrance are discussed.

REFERENCES

• 1: ~AINSWORTH, M., CRUIffKSHANK, A. H, GROVES, L. J, AND WALI,IS, P J L. 1994. Vmwpolnt ~specification and Z. Inf Softw. Tech. 36, 1, 43 51.
• 2: Alex Borgida , John Mylopoulos , Raymond Reiter, “…And nothing else changes”: the frame problem in procedure specifications, Proceedings of the 15th international conference on Software Engineering, p.303-314, May 17-21, 1993, Baltimore, Maryland, United States
• 3: ~DERRICK, J., }BOWMAN, H., AND STEEN, M. 1995. Maintaining cross-viewpoint consistency using ~Z. In the IFIP International Conference on Open Dzstmbuted Processtng. Chapman and Hail, ~395-406.
• 4: S. Easterbrook , B. Nuseibeh, Managing inconsistencies in an evolving specification, Proceedings of the Second IEEE International Symposium on Requirements Engineering, p.48, March 27-29, 1995
• 5: ~FINKELSTEIN, A., KRAMER, J., NUSEIBEH, B., FINKELSTEIN, L, AND GOEDICKE, M. 1992. View- ~points A framework for integrating multiple perspectives m system development. Int. J. ~Softw. Eng. Knowl. Eng 2, 1, 31 57.
• 6: ~FLINN, B. AND SORENSEN, I. H. 1993. Specificatton Case Studies, I. Hayes, Ed., 2nd ed. ~Prentme-Hall, Englewood Cliffs, N.J., chapter 5.
• 7: ~GARLAN, D. 1987. Views for tools in integrated cnvironraents. Tech. Rep. CUM-CS-87-147, ~School for Computer Science, Carnegie Mellon Umv., Pittsburgh, Pa. May.
• 8: ~GUTTAG, J., HORNING, J, AND WING, J. 1985. The Larch family of spemfication languages. ~IEEE Softw. 2, 5 (Sept.)
• 9: ~GUTTAG, J. V., HORNiNG, J. J., AND MODEL, A. 1990, Report on the Larch shared language: ~Version 2.3. Tech. Rep. 58, Digqtal Systems Research Center, Pale Alto, Calif. April.
• 10: ~HAB~:RMANN, A. N., KgUEGER, C., PmRcr:, B., STAUDT, B., AND WENN, J. 1988. Programming ~with views. Tech. Rep. CMU-CS-87-177, School of Computer Science, Carnegie Mellon Univ., ~Pittsburgh, Pa. Jan.
• 11: ~HALL.~ A. 1993. A response to Florence, Dougal and Zebedee. FACS Eur. 1, I (Fall).
• 12: HAYES, I. 1992. VDM and Z: A comparative case study. Formal Aspects Comput. 4, 1.
• 13: HAYES, I., Ed. 1993. Speclfwation Case Studtes, 2nd ed. Prentice-Hall, Englewood Cliffb, N J.
• 14: ~HAYES, I. J., JONES, C. B., AND NICHOLLS, J.E. 1993. Understanding the differences between ~VDM and Z. FACS Eur. 1, i (Fall).
• 15: C. A. R. Hoare, Programs are predicates, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.141-155, June 1985, London, United Kingdom
• 16: M. A. Jackson, Software development method, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 17: ~JACKSON, D. AND JACKSON, M. 1995. Problem decomposition for reuse. Tech Rep. CMU-CS-TR- ~95-108, School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa. Jan. To appear in ~Software En$ineering Journal.
• 18: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 19: Tom Maibaum , J. Fiadeiro , S. Khosla, Temporal reasoning over deontic specifications, Deontic logic in computer science: normative system specification, John Wiley and Sons Ltd., Chichester, UK, 1994
• 20: ~MORGAN, C. 1993. Spectftcatlon Case Studies, I. Hayes, Ed, 2nd ed. Prentice-Hall. Englewood ~Cliffs, N.J., chapter 3.
• 21: ~MORGAN, C. C. ANn SUFRIN, B. A, 1984, Specification of the UNIX filing system. IEEE Trans. ~Softw. Eng. SEJO, 2.
• 22: ~NORD, R.L. 1992. Deriving and manipulating module interfaces. Tech. Rep. CMU-CS-92-126, ~School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa. May.
• 23: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 24: ~SUFRIN, B. 1982. Formal specification of a display-oriented text editor. Sci. Comput. Program. ~1. 157-202
• 25: Nigel Ward, Adding Specification Constructors to the Refinement Calculus, Proceedings of the First International Symposium of Formal Methods Europe on Industrial-Strength Formal Methods, p.652-670, April 19-23, 1993
• 26: ~WOOt~COCK, J. C.P. 1989. Mathematics as a management tool: Proof rules for promotion. In ~Proceedings of the Centre for Software Rehabthty Conference: Large Software Systems (Bristol, ~U.K., Sept.). Centre fbr Software Reliability. {city}.
• 27: Jim Woodcock , Martin Loomes, Software engineering mathematics, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 28: Pamela Zave, A distributed alternative to finite-state-machine specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.10-36, Jan. 1985 [doi>10.1145/2363.2365]
• 29: Pamela Zave , Michael Jackson, Conjunction as composition, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.4, p.379-411, Oct. 1993 [doi>10.1145/158431.158438]
• 30: ~ZAVE, P. AND JACKSON, M. 1994. Where do operations come from? A multiparadigm specifica- ~tion t~chniqu~. Tech. Mern., AT&:T l~ell Laborat~or~es, Murray Hill, N.J. April.

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.1 Requirements/Specifications
          Subjects: Languages; Methodologies (e.g., object-oriented, structured)
        D.2.10 Design**
            Subjects: Representation**
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Algorithms, Languages

Keywords:
Z, formal specification, implicit definition, views