A Monad for Basic Java Semantics

  • Bart Jacobs
  • Erik Poll
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


This paper describes the role of a computational monad in the denotational semantics of sequential Java and investigates some of its properties. This denotational semantics is an abstraction of the one used for the verification of (sequential) Java programs using proof tools, see [11,15].


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. Alves-Foss and F. S. Lam. Dynamic Denotational Semantics of Java. In Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes Comp. Sci., pages 201–240. Springer-Verlag, 1998.Google Scholar
  2. 2.
    J. van den Berg, M. Huisman, B. Jacobs, and E. Poll. A type-theoretic memory model for verification of sequential Java programs. Techn. Rep. CSI-R9924, Comput. Sci. Inst., Univ. of Nijmegen, 1999.Google Scholar
  3. 3.
    P. Cenciarelli. An algebraic view of program composition. In A.M. Haeberer, editor, Algebraic Methodology and Software Technology, number 1548 in Lect. Notes Comp. Sci., pages 325–340. Springer, Berlin, 1998.CrossRefGoogle Scholar
  4. 4.
    M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge Univ. Press, 1996.Google Scholar
  5. 5.
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.Google Scholar
  6. 6.
    M. Huisman and B. Jacobs. Inheritance in Higher Order Logic: Modeling and Reasoning. Techn. Rep. CSI-R0004, Comput. Sci. Inst., Univ. of Nijmegen, 2000.Google Scholar
  7. 7.
    M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In Fundamental Approaches to Software Engineering, number 1783 in Lect. Notes Comp. Sci. Springer, Berlin, 2000.CrossRefGoogle Scholar
  8. 8.
    M. Huisman, B. Jacobs, and J. van den Berg. A case study in class library verification: Java’s Vector class. In B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs. Proceedings of the ECOOP’99 Workshop, pages 37–44. Techn. Rep. 251, Fernuniversität Hagen, 1999.Google Scholar
  9. 9.
    B. Jacobs. Inheritance and cofree constructions. In P. Cointe, editor, European Conference on Object-Oriented Programming, number 1098 in Lect. Notes Comp. Sci., pages 210–231. Springer, Berlin, 1996.Google Scholar
  10. 10.
    B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222–259, 1997.zbMATHGoogle Scholar
  11. 11.
    B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about classes in Java (preliminary report). In Object-Oriented Programming, Systems, Languages and Applications, pages 329–340. ACM Press, 1998.Google Scholar
  12. 12.
    E. Moggi. Notions of computation and monads. Inf. & Comp., 93(1):55–92, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    S. Owre, J.M. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw. Eng., 21(2):107–125, 1995.CrossRefGoogle Scholar
  14. 14.
    L.C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and computer science, pages 361–386. Academic Press, London, 1990. The APIC series, vol. 31.Google Scholar
  15. 15.
  16. 16.
    H. Reichel. An approach to object semantics based on terminal co-algebras. Math. Struct. in Comp. Sci., 5:129–152, 1995.zbMATHMathSciNetCrossRefGoogle Scholar
  17. 17.
    J.E. Stoy. Denotational Semantics: the Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, MA, 1977.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Bart Jacobs
    • 1
  • Erik Poll
    • 1
  1. 1.Dept. of Computer ScienceUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations