Advertisement

Abstract

Inheritance is one of the key features for the success of object-oriented languages. Inheritance (or specialisation) supports incremental design and re-use of already written specifications or programs. In a formal approach to system design the interest does not only lie in re-use of class definitions but also in re-use of correctness proofs. If a provably correct class is specialised we like to know those correctness properties which are preserved in the subclass. This can avoid re-verification of already proven properties and may thus substantially reduce the verification effort.

In this paper we study the question of inheritance of correctness properties in the context of state-based formalisms, using a temporal logic (CTL) to formalise requirements on classes. Given a superclass and its specialised subclass we develop a technique for computing the set of formulas which are preserved in the subclass. For specialisation we allow addition of attributes, modification of existing as well as extension with new methods.

Keywords

Temporal Logic Atomic Proposition Correctness Proof Kripke Structure Correctness Property 
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.

References

  1. 1.
    Browne, M.C., Clarke, E.M., Grumberg, O.: Characterising Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science 59, 115–131 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)Google Scholar
  3. 3.
    Dams, D.: Flat Fragments of CTL and CTL  ∗ : Separating the Expressive and Distinguishing Powers. Logic Journal of IGPL 7(1), 55–78 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. In: Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 118–129. IEEE Computer Society Press, Los Alamitos (1990)CrossRefGoogle Scholar
  5. 5.
    Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronisation skeletons. Science of Computer Programming 2(3), 241–266 (1982)CrossRefzbMATHGoogle Scholar
  6. 6.
    Emerson, E.A., Srinivasan, J.: Branching time temporal logic. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 123–171. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  7. 7.
    Hatcliff, J., Dwyer, M., Zheng, H.: Slicing software for model construction. Higher-order and Symbolic Computation (to appear)Google Scholar
  8. 8.
    Huizing, K., Kuiper, R.: Reinforcing fragile base classes. In: Poetzsch-Heffter, A. (ed.) Workshop on Formal Techniques for Java Programs, ECOOP 2001 (2001)Google Scholar
  9. 9.
    Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32, 705–778 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Liskov, B., Wing, J.: A behavioural notion of subtyping. ACM Transactions on Programming Languages and Systems 16(6), 1811–1841 (1994)CrossRefGoogle Scholar
  11. 11.
    Oda, T., Araki, K.: Specification slicing in formal methods of software development. In: Proceedings of the Seventeenth Annual International Computer Software & Applications Conference, pp. 313–319. IEEE Computer Society Press, Los Alamitos (1993)Google Scholar
  12. 12.
    Poetzsch-Heffter, A., Meyer, J.: Interactive verification environments for objectoriented languages. Journal of Universal Computer Science 5(3), 208–225 (1999)Google Scholar
  13. 13.
    Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)CrossRefzbMATHGoogle Scholar
  14. 14.
    van Glabbeek, R., Weijland, W.P.: Refinement in branching time semantics. In: Proc. IFIP Conference, pp. 613–618. North-Holland Publishing Company, Amsterdam (1989)Google Scholar
  15. 15.
    Wehrheim, H.: Behavioural subtyping and property preservation. In: Smith, S., Talcott, C. (eds.) FMOODS 2000: Formal Methods for Open Object-Based Distributed Systems. Kluwer, Dordrecht (2000)Google Scholar
  16. 16.
    Winter, K., Smith, G.: Compositional Verification for Object-Z. In: Bert, D., Bowen, J.P., King, S., Walden, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 280–299. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Heike Wehrheim
    • 1
  1. 1.Fachbereich InformatikUniversität OldenburgOldenburgGermany

Personalised recommendations