Advertisement

Reasoning and refinement in object-oriented specification languages

  • K. Lano
  • H. Haughton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 615)

Abstract

This paper describes a formal object-oriented specification language, Z++, and identifies proof rules and associated specification structuring and development styles for the facilitation of validation and verification of implementations against specifications in this language. We give inference rules for showing that certain forms of inheritance lead to refinement, and for showing that refinements are preserved by constructs such as promotion of an operation from a supplier class to a client class. Extension of these rules to other languages is also discussed.

Keywords

Communicate Sequential Process Data Refinement Algebraic Constraint Multiple Inheritance Predicate Transformer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    A. Alencar, J. Goguen: OOZE: An Object-Oriented Z Environment. In: P. America (ed.): ECOOP '91 Proceedings, Springer-Verlag LNCS, Vol 512, 1991.Google Scholar
  2. [2]
    R.J.R Back, A Calculus of Refinements for Program Derivation, Acta Informatica 25, 593–624 (1988).zbMATHMathSciNetCrossRefGoogle Scholar
  3. [3]
    J.L. Bell, Boolean-valued models and independence proofs in set theory, Oxford Logic Guides 12, Clarendon Press, Oxford 1977.Google Scholar
  4. [4]
    P. Breuer, K. Lano, From Code to Z Specifications. In: J. Nicholls (ed.): Z User Meeting 1989, in Springer-Verlag Workshops in Computer Science, 1990.Google Scholar
  5. [5]
    P. Breuer, K. Lano, Creating Specifications from Code: Reverse-Engineering Techniques, Journal of Software Maintenance, September 1991.Google Scholar
  6. [6]
    E. Cusack, Object-Oriented Modelling in Z. In: P. America (ed.): ECOOP '91 Proceedings, Springer-Verlag Lecture Notes in Computer Science, Vol 512, 1991.Google Scholar
  7. [7]
    A. Diller, Z: An Introduction to Formal Methods, Wiley, 1991.Google Scholar
  8. [8]
    D. Duke, R. Duke, P. King, G. A. Rose, G. Smith, Object-Z: An Object-Oriented Extension to Z, technical report 91-1, Software Verification Research Centre, The University of Queensland.Google Scholar
  9. [9]
    R. Duke, P. King, G. Smith, Formalising Behavioural Compatibility for Reactive Object-Oriented Systems. In: P. America (ed.): ECOOP '91 Proceedings, Springer-Verlag Lecture Notes in Computer Science, Vol. 512, 1991.Google Scholar
  10. [10]
    H. Haughton, K. Lano, An Algebraic Semantics for the Specification Language Z ++, AMAST '91 Conference, Iowa. To appear in Springer-Verlag Workshops in Computer Science.Google Scholar
  11. [11]
    H. Haughton, K. Lano, Using Formal Methods in Artificial Intelligence, IJCAI '91 Workshop on Software Engineering for Knowledge-Based Systems, Sydney, August 1991.Google Scholar
  12. [12]
    C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall 1985.Google Scholar
  13. [13]
    K. Lano, H. Haughton, P. Breuer, Reverse-Engineering of Library Case Study, REDO Document 2487-TN-PRG-1064, April 1991.Google Scholar
  14. [14]
    K. Lano, H. Haughton, Axioms for Object-Oriented Extensions to Z, ZOOM Workshop, Oxford University Programming Research Group, 1991.Google Scholar
  15. [15]
    K. Lano, Z ++, an Object-Oriented Extension to Z. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 151–172, 1991.Google Scholar
  16. [16]
    K. Lano, The Design of the Verification Toolset, REDO Project Document 2487-TN-PRG-1068, Oxford University Programming Research Group, 1991.Google Scholar
  17. [17]
    K. Lano, Integrating Development and Maintenance in an Object-Oriented Environment, REDO Document 2487-TN-PRG-1050, Oxford University Programming Research Group, 1991.Google Scholar
  18. [18]
    S. Leonard, J. Pardoe, S. Wade, Software Maintenance — Cinderella is Still not Getting to the Ball. In: BCS/IEE Conference on Software Engineering 1988, IEE London, 104–106, 1988.Google Scholar
  19. [19]
    P. Lupton, Promoting Forward Simulation. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 1991.Google Scholar
  20. [20]
    J. A. McDermid, P. J. Whysall, Object Oriented Specification and Refinement. In: Proceedings of the 4th Refinement Workshop, Cambridge, Springer-Verlag Workshops in Computing, 1991.Google Scholar
  21. [21]
    S. Meira, A.L.C. Cavalcanti, Modular Object-oriented Z Specifications. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 1991.Google Scholar
  22. [22]
    B. Meyer, Tools for the New Culture: Lessons from the Design of the Eiffel Libraries, Communications of the ACM, September 1990, Vol 33, No. 9.Google Scholar
  23. [23]
    D. Monk, Mathematical Logic, North Holland, 1979.Google Scholar
  24. [24]
    C. Morgan, K. Robinson, P. Gardiner, On The Refinement Calculus, PRG Monograph PRG-70, 1988, Oxford University Programming Research Group.Google Scholar
  25. [25]
    J. M. Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, 9(3), 298–306, December 1987.CrossRefGoogle Scholar
  26. [26]
    D. Neilson, Machine Support for Z: the zedB tool, Z User Meeting 1990. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 1991.Google Scholar
  27. [27]
    C. Stanley-Smith, A. Cahill, UNIFORM: A Language Geared To System Description and Transformation, University of Limerick, 1990.Google Scholar
  28. [28]
    I. SØrensen, The B Method, VDM '91, Noodwijkerhout, Netherlands, 1991.Google Scholar
  29. [29]
    M. Spivey, Understanding Z, CUP, Cambridge, 1988.Google Scholar
  30. [30]
    M. Spivey, The Z Notation: A Reference Manual, Prentice Hall 1989.Google Scholar
  31. [31]
    A. Wills, Capsules and Types in Fresco. In: P. America (ed.): ECOOP '91 Proceedings, Springer Verlag Lecture Notes in Computer Science, Vol 512, 1991.Google Scholar
  32. [32]
    J. Woodcock, S. Brien, W: A Logic for Z, Oxford University Programming Research Group, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • K. Lano
    • 1
  • H. Haughton
    • 1
  1. 1.Lloyds Register of ShippingCroydon

Personalised recommendations