Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-22T04:26:19.709Z Has data issue: false hasContentIssue false
  • English
  • Français

Observable interface behaviour and inheritance

Published online by Cambridge University Press:  13 November 2014

ERIKA ÁBRAHÁM ,
THI MAI THUONG TRAN  and
MARTIN STEFFEN
ERIKA ÁBRAHÁM
Affiliation:
Computer Science Department, RWTH Aachen University, Aachen Email: [email protected]
THI MAI THUONG TRAN
Affiliation:
RWTH Aachen University, Informatik 2, D-52056 Aachen, Germany Email: [email protected]
MARTIN STEFFEN
Affiliation:
University of Oslo, Department of Informatics, P.O. Box 1080 Blindern, N-0316 Oslo Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper formalizes the observable interface behaviour of open systems for a strongly-typed, concurrent object-oriented language with single-class inheritance. We formally characterize the observable behaviour in terms of interactions at the program-environment interface. The behaviour is given by transitions between contextual judgments, where the absent environment is represented abstractly as assumption context. A particular challenge is the fact that, when the system is considered as open, code from the environment can be inherited to the component and vice versa. This requires to incorporate an abstract version of the heap into the environment assumptions when characterizing the interface behaviour. We prove the soundness of the abstract interface description.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 3: Special Issue: Behavioural Types Part 2 , March 2016 , pp. 561 - 605
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M. and Cardelli, L. (1996) A Theory of Objects, Monographs in Computer Science, Springer-Verlag.Google Scholar
Ábrahám, E., de Boer, F. S., Bonsangue, M. M., Grüner, A. and Steffen, M. (2005) Observability, connectivity, and replay in a sequential calculus of classes. In: Bonsangue, M., de Boer, F. S., de Roever, W.-P. and Graf, S. (eds.) Proceedings of the 3rd International Symposium on Formal Methods for Components and Objects (FMCO 2004). Springer-Verlag Lecture Notes in Computer Science 3657 296–316 (21 pages). Available at http://www.ifi.uio.no/~msteffen/download/fa-fmco.pdf.Google Scholar
Ábrahám, E., Grüner, A. and Steffen, M. (2006) Abstract interface behavior of object-oriented languages with monitors. In: Gorrieri, R. and Wehrheim, H. (eds.) FMOODS'06. Springer-Verlag Lecture Notes in Computer Science 4037 218–232 (15 pages). Available at http://www.springerlink.com/content/3365g26781740807.CrossRefGoogle Scholar
Ábrahám, E., Grabe, I., Grüner, A. and Steffen, M. (2007) Behavioral interface description of an object-oriented language with futures and promises. Journal of Logic and Algebraic Programming 78 (7) 491–518 (28 pages). Available at http://www.ifi.uio.no/~msteffen/download/09/futures.pdf. (Special issue with selected contributions of NWPT'07. The paper is a reworked version of an earlier UiO Technical Report TR-364.)CrossRefGoogle Scholar
Ábrahám, E., Grüner, A. and Steffen, M. (2008) Abstract interface behavior of object-oriented languages with monitors. Theory of Computing Systems 43 (3–4) 322–361 (40 pages). Available at http://www.ifi.uio.no/~msteffen/download/07/monitors-tocs.pdf.CrossRefGoogle Scholar
Abramsky, S. and McCusker, G. (1996) Linearity, sharing, and state: A fully abstract game semantics for Idealized Algol with active expressions (extended abstract). volume 2. Birkhäuser, two volumes, 1997. (Reprint of the paper which appeared in the Proceedings of the 1996 Workshop on Linear Logic. Electronic Notes in Theoretical Computer Science 3.)Google Scholar
Agha, G. and Hewitt, C. (1987) Concurrent programming using actors. In: Object-Oriented Concurrent Programming, MIT Press 37–53.Google Scholar
Ahrendt, W. and Dylla, M. (2012) A system for compositional verification of asynchronous objects. Science of Computer Programming 77 (12) 1289–1309 ISSN . Available at http://www.sciencedirect.com/science/article/pii/S0167642310001553.Google Scholar
Armstrong, J., Virding, R., Wikström, C. and Williams, M. (1996) Concurrent Programming in Erlang, 2nd edition, Prentice Hall Europe, Hemel Hempstead, Hertfordshire.Google Scholar
Banerjee, A. and Naumann, D. A. (2005) Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM 52 (6) 894–960 ISSN .CrossRefGoogle Scholar
Breazu-Tannen, V., Gunter, C. A. and Ščedrov, A. (1990) Computing with coercions. In: Proceedings of the ACM Conference on Lisp and Functional Programming 44–61.CrossRefGoogle Scholar
Cook, W. (1989) A Denotational Model of Inheritance, Ph.D. thesis, Brown University.Google Scholar
Curien, P.-L. (2007) Definability and full abstraction. Electronic Notes in Theoretical Computer Science 172 301–310 ISSN . Available at http://dx.doi.org/10.1016/j.entcs.2007.02.011.Google Scholar
de Boer, F. S., Clarke, D. and Johnsen, F. B. (2007) A complete guide to the future. In: de Nicola, R. (eds.) Proceedings of Programming Languages and Systems, 16th European Symposium on Programming, Vienna, Austria. Springer-Verlag Lecture Notes in Computer Science 4421 316–330.Google Scholar
Din, C. C., Dovland, J. and Owe, O. (2012) Compositional reasoning about shared futures. In: Proceedings of SEFM'12. Springer-Verlag Lecture Notes in Computer Science 7504 94–108. ISBN 978-3-642-33825-0.CrossRefGoogle Scholar
Donahue, J. (1979) On the semantics of data type. SIAM J. Computing 8 546–560.CrossRefGoogle Scholar
Gordon, A. D., Hankin, P. D. and Lassen, S. B. (1997) Compilation and equivalence of imperative objects. In: Ramesh, S. and Sivakumar, G. (eds.) Proceedings of FSTTCS'97. Springer-Verlag Lecture Notes in Computer Science 1346 74–87. (Full version available as Technical Report 429, University of Cambridge Computer Laboratory, June 1997.)Google Scholar
Gordon, A. D. and Rees, G. D. (1996) Bisimilarity for a first-order calculus of objects with subtyping. In: Proceedings of POPL '96, ACM 386–395. (Full version available as Technical Report 386, Computer Laboratory, University of Cambridge.)Google Scholar
Haynes, C. T. (1984) A theory of data type representation independence. In: Kahn, K., MacQueen, D. and Plotkin, G. D. (eds.) Semantics of Data Types. Springer-Verlag Lecture Notes in Computer Science 173 157–176.Google Scholar
Jeffrey, A. and Rathke, J. (2002) A fully abstract may testing semantics for concurrent objects. In: Proceedings of LICS '02, IEEE, Computer Society Press 101–112.Google Scholar
Jeffrey, A. and Rathke, J. (2005) Java Jr.: A fully abstract trace semantics for a core Java language. In: Sagiv, M.(eds.) Proceedings of ESOP 2005. Springer-Verlag Lecture Notes in Computer Science 3444 423–438.CrossRefGoogle Scholar
Kamin, K. (1988) Inheritance in Smalltalk-80: A denotational definition. In: ACM Conference on Programming Language Design and Implementation (PLDI) (Atlanta, GA), ACM in SIGPLAN Notices 23 (7).Google Scholar
Koutavas, V. and Wand, M. (2007) Reasoning about class behavior. In: Informal Workshop Record of FOOL 2007.Google Scholar
Kurnia, I. W. and Poetzsch-Heffter, A. (2013) Verification of open concurrent object systems. In: de Boer, F. S., Bonsangue, M. M., Giachino, E. and Hähnle, R. (eds.) Proceedings of the 11th International Symposium on Formal Methods for Components and Objects, FMCO 2012. Springer-Verlag Lecture Notes in Computer Science 7866 83–118.Google Scholar
Mikhajlov, L. and Sekerinski, E. (1998) A study of the fragile base class problem. In: Proceedings of the 12th European Conference on Object-Oriented Programming (ECOOP'98), Brussels, Belgium. Springer-Verlag Lecture Notes in Computer Science 1445 355–354.Google Scholar
Mitchell, J. C. (1986) Representation independence and data abstraction. In: 13th Annual Symposium on Principles of Programming Languages (POPL) (St. Peterburg Beach, FL), ACM 263–276.CrossRefGoogle Scholar
Odersky, M., Spoon, L. and Venners, B. (2011) Programming in Scala, Artima Series, Artima Press. ISBN 9780981531649. Available at http://books.google.no/books?id=ZNo8cAAACAAJ.Google Scholar
Poetzsch-Heffter, A. and Schäfer, J. (2007) A representation-independent behavioral semantics for object-oriented components. In: Bonsangue, M. M. and Johnsen, E. B. (eds.) FMOODS'07. Springer-Verlag Lecture Notes in Computer Science 4468 157–173.Google Scholar
Reddy, U. S. (1988) Objects as closures: Abstract semantics of object-oriented languages. In: Symposium on lisp and Functional Programming (Snowbird, UT), ACM 289–297.Google Scholar
Reynolds, J. (1974) Towards a theory of type structure. In: Robinet, B. (ed.) Colloque sur la Programmation (Paris, France). Springer-Verlag Lecture Notes in Computer Science 19 408–425.Google Scholar
Reynolds, J. (1983) Types, abstraction, and parametric polymorphism. In: Mason, R. E. A. (ed.) Information Processing 83, IFIP, North-Holland 513–523.Google Scholar
Ruby, C. and Leavens, G. T. (2000) Safely creating correct subclasses without seeing superclass code. In: Object Oriented Programming: Systems, Languages, and Applications (OOPSLA)'00, ACM 208–228. (In SIGPLAN Notices.)Google Scholar
Snyder, A. (1986) Encapsulation and inheritance in object-oriented programming languages. In: Object Oriented Programming: Systems, Languages, and Applications (OOPSLA)'86 (Portland, Oregon), ACM 38–45. (In SIGPLAN Notices 21 (11).)Google Scholar
Stata, R. and Guttag, J. V. (1995) Modular reasoning in the presence of subclassing. In: Object Oriented Programming: Systems, Languages, and Applications (OOPSLA)'95, ACM 200–214. (In SIGPLAN Notices 30 (10).)CrossRefGoogle Scholar
Viswanathan, R. (1998) Full abstraction for first-order objects with recursive types and subtyping. In: Proceedings of LICS '98. IEEE, Computer Society Press.Google Scholar
Welsch, Y. and Poetzsch-Heffter, A. (2014) A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries. Science of Computer Programming, (Selected papers from the Brazilian Symposium on Formal Methods (SBMF 2011)) 92, Part B, 129–161 ISSN . Available at http://www.sciencedirect.com/science/article/pii/S0167642313002529. (Available online 25 October 2013.)Google Scholar