Abstract interface behavior of object-oriented languages with monitors. (English) Zbl 1162.68475

Summary: We characterize the observable behavior of multi-threaded, object-oriented components with re-entrant monitors. We show that a compositional approach leads to observable uncertainty wrt. monitor operations at the interface which we capture by may- and must-approximations for potential, resp. necessary lock ownership. The concepts are formalized in an object calculus. We show the soundness of the abstractions.


68Q55 Semantics in the theory of computing


Z; Java Jr
Full Text: DOI Link


[1] Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, New York (1996) · Zbl 0876.68014
[2] Ábrahám, E., Bonsangue, M.M., de Boer, F.S., Steffen, M.: Object connectivity and full abstraction for a concurrent calculus of classes. In: Li, Z., Araki, K. (eds.) ICTAC’04. Lecture Notes in Computer Science, vol. 3407, pp. 37–51. Springer, New York (2004) · Zbl 1108.68538
[3] Ábrahám, E., de Boer, F.S., Bonsangue, M.M., Grüner, A., Steffen, M.: Observability, connectivity, and replay in a sequential calculus of classes. In: Bonsangue, M., de Boer, F.S., de Roever, W.-P., Graf, S. (eds.) Proceedings of the Third International Symposium on Formal Methods for Components and Objects (FMCO 2004). Lecture Notes in Computer Science, vol. 3657, pp. 296–316. Springer, New York (2005) · Zbl 1143.68359
[4] Ábrahám, E., Grüner, A., Steffen, M.: Dynamic heap-abstraction for open, object-oriented systems with thread classes. SoSYM J. (2007, accepted). This is a reworked version of the Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel technical report nr. 0601 and an extended version of the CiE’06 extended abstract
[5] America, P.: Issues in the design of a parallel object-oriented language. Formal Aspects Comput. 1(4), 366–411 (1989) · Zbl 0694.68012
[6] Brinch Hansen, P.: Operating System Principles. Prentice-Hall, Englewood Cliffs (1973) · Zbl 0308.68007
[7] de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: de Nicola, R. (ed.) Proceedings of Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Vienna, Austria. Lecture Notes in Computer Science, vol. 4421, pp. 316–330 (2007)
[8] de Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984) · Zbl 0985.68518
[9] ECMA International Standardizing Information and Communication Systems: C# Language Specification, 2nd edn. (Dec. 2002). Standard ECMA-334
[10] Gordon, A.D., Hankin, P.D.: A concurrent object calculus: reduction and typing. In: Nestmann, U., Pierce, B.C. (eds.) Proceedings of HLCL ’98. Electronic Notes in Theoretical Computer Science, vol. 16.3. Elsevier, Amsterdam (1998) · Zbl 0917.68064
[11] Gosling, J., Joy, B., Steele, G.L., Bracha, G.: The Java Language Specification, 2nd edn. Addison-Wesley, Reading (2000) · Zbl 0865.68001
[12] Hoare, C.A.R.: Monitors: an operating system structuring concept. Commun. ACM 17(10), 549–557 (1974) · Zbl 0308.68029
[13] Jeffrey, A., Rathke, J.: A fully abstract may testing semantics for concurrent objects. In: Proceedings of LICS ’02. IEEE Computer Society Press (July 2002) · Zbl 1078.68107
[14] Jeffrey, A., Rathke, J.: Java Jr.: a fully abstract trace semantics for a core Java language. In: Sagiv, M. (ed.) Proceedings of ESOP 2005. Lecture Notes in Computer Science, vol. 3444, pp. 423–438. Springer, New York (2005) · Zbl 1108.68349
[15] Koutavas, V., Wand, M.: Bisimulations for untyped imperative objects. In: Sestoft, P. (ed.) Proceedings of Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2005, Vienna, Austria. Lecture Notes in Computer Science, vol. 3924, pp. 146–161. Springer (2005) · Zbl 1178.68154
[16] Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Proceedings of POPL ’06, pp. 141–152. ACM (Jan. 2006) · Zbl 1178.68154
[17] Koutavas, V., Wand, M.: Reasoning about class behavior. In: Informal Workshop Record of FOOL 2007 (Jan. 2007)
[18] Milner, R.: Fully abstract models of typed {\(\lambda\)}-calculi. Theor. Comput. Sci. 4, 1–22 (1977) · Zbl 0386.03006
[19] Morris, J.H.: Lambda calculus models of programming languages. Ph.D. thesis, MIT (1968)
[20] Olderog, E.-R., Hoare, C.A.R.: Specification-oriented semantics of communicating processes. Acta Inf. 23(1), 9–66 (1986). A preliminary version appeared under the same title in the proceedings of the 10th ICALP 1983, volume 154 of LNCS · Zbl 0569.68019
[21] Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5, 223–255 (1977) · Zbl 0369.68006
[22] Poetzsch-Heffter, A., Schäfer, J.: A representation-independent behavioral semantics for object-oriented components. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS ’07. Lecture Notes in Computer Science, vol. 4468. Springer, New York (2007) · Zbl 1202.68100
[23] Potter, B.F., Sinclair, J.E., Till, D.: An Introduction to Formal Specification and Z. Series in Computer Science. Prentice-Hall, Englewood Cliffs (1990) · Zbl 0860.68069
[24] Smith, G.P.: An object-oriented approach to formal specification. Ph.D. thesis, Department of Computer Science, University of Queensland (Oct. 1992)
[25] Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989) · Zbl 0777.68003
[26] Steffen, M.: Object-connectivity and observability for class-based, object-oriented languages. Habilitation thesis, Technische Faktultät der Christian-Albrechts-Universität zu Kiel (2006), submitted 4th July, accepted 7 February 2007
[27] The Creol language. http:www.ifi.uio.no/\(\sim\)creol (2007)
[28] Viswanathan, R.: Full abstraction for first-order objects with recursive types and subtyping. In: Proceedings of LICS ’98. IEEE Computer Society Press (July 1998)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.