From Astrophysics to Unconventional Computation pp 255-298 | Cite as

# Sound and Relaxed Behavioural Inheritance

## Abstract

Object-oriented (OO) inheritance establishes taxonomies of OO classes. Behavioural inheritance (BI), a strong version, emphasises substitutability: objects of child classes replace objects of their ascendant classes without any observable effect difference on the system. BI is related to data refinement, but refinement’s constrictions rule out many useful OO subclassings. This paper revisits BI at the light of Z and the theory of data refinement. It studies existing solutions to this problem, criticises them, and proposes improved relaxations. The results are applicable to any OO language that supports design-by-contract (DbC). The paper’s contributions include three novel BI relaxations supported by a mathematical model with proofs carried out in the Isabelle proof assistant, and an examination of BI in the DbC languages Eiffel, JML and Spec\(\sharp \).

## Keywords

Refinement Z Object-orientation Inheritance Design-by-contract JML Eiffel Spec\(\sharp \) Behavioural subtyping## Notes

### Acknowledgements

The work presented here commenced when I was a Ph.D. student at the University of York supervised by Prof. Susan Stepney and Dr. Fiona Polack. I am very happy that this paper is part of this volume because Susan Stepney was immensely influential and inspiring not only to the whole work presented here, but to myself and my academic work.

## Supplementary material

## References

- 1.Abrial, J.R., Cansell, D., Méry, D.: Refinement and reachability in Event\(\_\)B. In: Proceedings of ZB2005. LNCS, vol. 3455, pp. 222–241. Springer (2005). https://doi.org/10.1007/11415787_14
- 2.Amálio, N.: Generative frameworks for rigorous model-driven development. Ph.D. thesis, Department Computer Science, University of York (2007)Google Scholar
- 3.Amálio, N.: Relaxing behavioural inheritance. In: Proceedings of Refine 2013, EPTCS, vol. 115, pp. 68–83 (2013)Google Scholar
- 4.Amálio, N.: Behavioural inheritance with relaxed but safe constraints grounded on data refinement. Technical report, Birmingham City University (2018). http://bit.ly/BI5nl0I
- 5.Amálio, N.: Isabelle proofs of behavioural inheritance and relaxations (2018). http://bit.ly/2o0KaI2
- 6.Amálio, N., Glodt, C.: A tool for visual and formal modelling of software designs. Sci. Comput. Program. Part 1
**98**, 52 – 79 (2015). https://doi.org/10.1016/j.scico.2014.05.002 - 7.Amálio, N., Glodt, C., Kelsen, P.: Building VCL models and automatically generating Z specifications from them. In: Proceedings of FM 2011. LNCS, vol. 6664, pp. 149–153. Springer (2011)Google Scholar
- 8.Amálio, N., Kelsen, P.: Modular design by contract visually and formally using VCL. In: Proceedings of VL/HCC 2010, pp. 227–234. IEEE (2010). https://doi.org/10.1109/VLHCC.2010.39
- 9.Amálio, N., Kelsen, P., Ma, Q., Glodt, C.: Using VCL as an aspect-oriented approach to requirements modelling. TAOSD
**VII**, 151–199 (2010)Google Scholar - 10.Amálio, N., Polack, F., Stepney, S.: An object-oriented structuring for Z based on views. In: Proceedings of ZB 2005. LNCS, vol. 3455, pp. 262–278. Springer (2005)Google Scholar
- 11.Amálio, N., Polack, F., Stepney, S.: UML+Z: Augmenting UML with Z. In: Abrias, H., Frappier, M. (eds.) Software Specification Methods. ISTE (2006)Google Scholar
- 12.Amálio, N., Polack, F., Stepney, S.: Frameworks based on templates for rigorous model-driven development. ENTCS
**191**, 3–23 (2007)Google Scholar - 13.Banach, R., Poppleton, M.: Retrenchment: an engineering variation on refinement. In: Proceedings of B’98. LNCS, vol. 1393, pp. 129–147. Springer (1998). https://doi.org/10.1007/BFb0053358
- 14.Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comput. Program.
**67**(2–3), 301–329 (2007)MathSciNetCrossRefGoogle Scholar - 15.Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., et al. (eds.) Proceedings of FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer (2006)Google Scholar
- 16.Derrick, J., Boiten, E.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer (2001)Google Scholar
- 17.Dhara, K.K., Leavens, G.T.: Forcing behavioural subtyping through specification inheritance. In: 18th International Conference on Software Engineering, ICSE-18, pp. 258–267. Also published as TR \(\#95-20c\), Department of Computer Science, Iowa State University, (1996)Google Scholar
- 18.Fischer, C., Wehrheim, H.: Behavioural subtyping relations for object-oriented formalisms. In: Proceedings of AMAST 2000. LNCS, vol. 1816, pp. 469–483. Springer (2000)Google Scholar
- 19.Hall, A.: Using Z as a specification calculus for object-oriented systems. In: Hoare, A., Bjørner, D., Langmaack, H. (eds.) Proceedings of VDM ’90. LNCS, vol. 428, pp. 290–318 (1990)Google Scholar
- 20.Hall, A.: Specifying and interpreting class hierarchies in Z. In: Z User Workshop, Workshops in Computing, pp. 120–138. Springer (1994)Google Scholar
- 21.Harel, D., Kupferman, O.: On object systems and behavioural inheritance. IEEE Trans. Softw. Eng.
**28**(9), 889–903 (2002)CrossRefGoogle Scholar - 22.He, J., Hoare, A., Sanders, J.W.: Data refinement refined. In: Proceedings of ESOP’86. LNCS, vol. 213, pp. 187–196. Springer (1986). https://doi.org/10.1007/3-540-16442-1_14
- 23.Hoare, A.: Proof of correctness of data representations. Acta Inform.
**1**(1), 271–281 (1972). https://doi.org/10.1007/BF00289507CrossRefzbMATHGoogle Scholar - 24.ISO: Information technology–Z formal specification notation–syntax, type system and semantics. ISO/IEC 13568:2002. International Standard (2002)Google Scholar
- 25.Jackson, D.: Software Abstractions: Logic, Lanaguage, and Analysis. MIT Press (2006)Google Scholar
- 26.Leavens, G.T.: JML’s rich, inherited specifications for behavioural subtypes. In: Proceedings of ICFEM 2006, vol. 4260, pp. 2–34. Springer (2006)Google Scholar
- 27.Leino, K.R.M., Müller, P.: Using the spec\(\#\) language, methodology, and tools to write bug-free programs. In: Advanced Lectures on Software Engineering: LASER Summer School 2007/2008, pp. 91–139. Springer (2010)Google Scholar
- 28.Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst.
**16**(6), 1811–1841 (1994)CrossRefGoogle Scholar - 29.Lupton, P.J.: Promoting forward simulation. In: Z User Workshop, pp. 27–49. Springer (1990)Google Scholar
- 30.Mayr, E.: Biological classification: toward a synthesis of opposing methodologies. Science
**214**(30) (1981)Google Scholar - 31.Meyer, B.: Applying “design by contract”. Computer
**25**(10), 40–51 (1992)Google Scholar - 32.Meyer, B.: Object-Oriented Software Construction. Prentice-Hall (1997)Google Scholar
- 33.Meyer, B.: Touch of Class: Learning to Program Well with Objects and Contracts. Springer (2009)Google Scholar
- 34.Smith, G.P.: The Object-Z Specification Language. Kluwer Academic Publishers (2000). https://doi.org/10.1007/978-1-4615-5265-9
- 35.Stepney, S., Polack, F., Toyn, I.: Patterns to guide practical refactoring: examples targetting promotion in Z. In: Proceedings of ZB 2003. LNCS, vol. 2651, pp. 20–39. Springer (2003)Google Scholar
- 36.Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Automatic verification of advanced object-oriented features: the autoproof approach. In: Proceedings of LASER 2012. LNCS, vol. 7682, pp. 133–155 (2012)Google Scholar
- 37.Wehrheim, H.: Behavioral subtyping and property preservation. In: Smith, S.F., Talcott, C.L. (eds.) Proceedings of FMOODS 2000, pp. 213–231. Kluwer (2000)Google Scholar
- 38.Wirth, N.: Program development by stepwise refinement. Commun. ACM
**14**(4), 221–227 (1971)CrossRefGoogle Scholar - 39.Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall (1996)Google Scholar