Skip to main content
SpringerLink
Log in

Formal Techniques for Java Programs

  • Conference paper
  • First Online:
Object-Oriented Technology ECOOP’99 Workshop Reader (ECOOP 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1743))

Included in the following conference series:

Abstract

This report explains the motivation for a workshop on formal techniques for Java programs. It gives an overview of the presentations and summarizes the results of the working groups. Furthermore, it contains abstracts of the contributed papers.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Cardelli. A Theory of Objects. Monographs in Computer Science. Springer-Verlag, New York, 1996. ISBN 0-387-94775-2.

    Google Scholar 

  2. M. Abadi and K.R.M. Leino. A logic of object-oriented programs. In M. Bidoit and M. Dauchet, (eds.): Proc. TAPSOFT’ 97, 7th Int. Joint Conference CAAP/FASE, vol. 1214, LNCS, pp. 682–696. Springer, 1997.

    Google Scholar 

  3. A. Aiken and N. Heintze, Constraint-based program analysis. Tutorial of 22th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Januaray 1995.

    Google Scholar 

  4. R. Allen and D. Garlan. A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology, 6(3):213–249, June 1997.

    Article  Google Scholar 

  5. J. Alves-Foss, (ed.): Formal Syntax and Semantics of Java. LNCS, vol. 1523, Springer, 1999.

    Google Scholar 

  6. K. Arnold and J. Gosling. The Java Programming Language. Addison-Wesley, 2nd edition, 1997.

    Google Scholar 

  7. D. Bartetzko. Parallelität und Vererbung beim ‘Programmieren mit Vertrag’. Master’s thesis, University of Oldenburg, May 1999. in German.

    Google Scholar 

  8. J. Bicarregui, K. Lano, and T. Maibaum: Towards a Compositional Interpretation of Object Diagrams. Technical Report, Department of Computing, Imperial College, 1997.

    Google Scholar 

  9. E. Börger and W. Schulte. A programmer friendly modular definition of the semantics of Java. http://www.informatik.uni-ulm.de/pm/mitarbeiter/wolfram.html.

  10. P. Cenciarelli. Computational applications of calculi based on monads. PhD thesis, Department of Computer Science, University of Edinburgh, 1995. CST-127-96._Also available as ECS-LFCS-96-346.

    Google Scholar 

  11. P. Cenciarelli. An Algebraic View of Program Composition. In Armando Haeberer, editor, Proceedings of 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98), 1998. LNCS 1548.

    Google Scholar 

  12. P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In Proceedings of 5th Biennial Meeting on Category Theory and Computer Science. CTCS-5, 1993. CWI Tech. Report.

    Google Scholar 

  13. P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. From sequential to multithreaded Java: an event-based operational semantics. In 6th Conf. Algebraic Methodology and Software Technology, AMAST, 1997.

    Google Scholar 

  14. P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. An Event-Based Structural Operational Semantics of Multi-Threaded Java. In [5].

    Google Scholar 

  15. S. Cimato. A Methodology for the Specification and Verification of Java Components and Architectures. PhD thesis, Dept. of Computer Science, University of Bologna, Italy, February 1999.

    Google Scholar 

  16. A.N. Clark and A.S. Evans: Semantic Foundations of the Unified Modelling Language. In the proceedings of the First Workshop on Rigorous Object-Oriented Methods: ROOM 1, Imperial College, June, 1997.

    Google Scholar 

  17. A.N. Clark: A Semantics for Object-Oriented Systems. Presented at the Third Northern Formal Methods Workshop. September 1998. In BCS FACS Electronic Workshops in Computing, 1999.

    Google Scholar 

  18. A.N. Clark: A Semantics for Object-Oriented Design Notations. Technical report, submitted to the BCS FACS Journal, 1999.

    Google Scholar 

  19. R. Cohen. Defensive Java Virtual Machine Specification. http://www.cli.com/software/djvm.

  20. E. Coscia and G. Reggio. An operational semantics for java. Departimento di Informatica e Scienze dell’ Informazione, Universita di Genova, http://www.disi.unige.it.

  21. F.S. de Boer. A wp-calculus for OO. In W. Thomas, (ed.), Foundations of Software Sci. and Comp. Struct., vol. 1578 of LNCS. Springer, 1999.

    Chapter  Google Scholar 

  22. G. DeFouw, D. Grove, and C. Chambers, Fast interprocedural class analysis, Proceedings of 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages pages 222–236, Januaray 1998.

    Google Scholar 

  23. E.W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976.

    MATH  Google Scholar 

  24. S. Drossopoulou and S. Eisenbach. Is the Java type system sound? In Fourth International Workshop on Foundations of Object-Oriented Languages, October 1997. http://www.outoften.doc.ic.ac.uk/projects/slurp/papers.html.

  25. S. Drossopoulou and S. Eisenbach. Java is type safe-probably. In 11th European Conference on Object-Oriented Programming, February 1997. http://www.outoften.doc.ic.ac.uk/projects/slurp/papers.html.

  26. S. Drossopoulou and S. Eisenbach. Towards an operational semantics and proof of type soundness for java, April 1998. http://www.outoften.doc.ic.ac.uk/projects/slurp/papers.html.

  27. R. Duke, G. Rose, and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17:511–533, 1995.

    Article  Google Scholar 

  28. Extended Static Checking home page, Compaq Systems Research Center. On the Web at http://www.research.digital.com/SRC/esc/Esc.html.

  29. C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS’ 97), volume 2, pages 423–438. Chapman & Hall, 1997.

    Google Scholar 

  30. J. Goguen: Objects. Int. Journal of General Systems, 1(4):237–243, 1975.

    Article  Google Scholar 

  31. J. Goguen: Sheaf Semantics for Concurrent Interacting Objects. Mathematical Structures in Computer Science, 1990.

    Google Scholar 

  32. A. Gontmakher and A. Schuster. Java consistency: Non-operational characterizations for java memory behaviour. Technical Report CS0922, Computer Science Department, Technion, November 1997.

    Google Scholar 

  33. J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.

    Google Scholar 

  34. J. Guttag and J. Horning. Larch: Languages and Tools for Formal Specification. Springer-Verlag, Berlin, 1993.

    MATH  Google Scholar 

  35. N. Heintze, Set-based program analysis. Ph.D thesis, Carnegie Mellon University, October 1992.

    Google Scholar 

  36. M. Hofmann and B. Pierce. Positive subtyping. Information and Computation, 126(1):186–197, 1996.

    Article  MathSciNet  Google Scholar 

  37. B. Jacobs. Coalgebraic reasoning about classes in object-oriented languages. In CMCS 1998, number 11 in Electr. Notes in Comp. Sci. Elsevier, 1998.

    Google Scholar 

  38. 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 (OOPSLA), pages 329–340. ACM Press, 1998.

    Google Scholar 

  39. B. Jacobs, G.T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors. Formal Techniques for Java Programs. Technical Report 251, Fernuniversität Hagen, 1999. URL: http://www.informatik.fernuni-hagen.de/pi5/publications.html.

  40. Jass: Java with assertions, May 1999. http://www.semantik.informatik.uni-oldenburg.de/~jass.

  41. C. Jones. A pi-calculus semantics for an object-based design notation. In Proc. of CONCUR’93, 1993. LNCS 715.

    Google Scholar 

  42. G.T. Leavens. Modular specification and verification of object-oriented programs. IEEE Software, 8(4):72–80, 1991.

    Article  Google Scholar 

  43. K.R.M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. Tech. Report KRML 65-0, SRC, 1996.

    Google Scholar 

  44. K.R.M. Leino. Recursive object types in a logic of object-oriented programs. Nordic Journal of Computing, 5(4):330–360, 1998.

    MATH  MathSciNet  Google Scholar 

  45. J. Magee, N. Dulay, S. Eisenbach, and J. Kramer. Specifying Distributed Software Architectures. In Proc. 5th European Software Engineering Conf. (ESEC 95), v. 989 of LNCS, pp. 137–153, Sitges, Spain, September 1995.

    Google Scholar 

  46. B. Meyer. Object-Oriented Software Construction. Prentice Hall, 1988.

    Google Scholar 

  47. R. Milner. Implementation and application of Scott’s logic of continuous functions. In Conf. on Proving Assertions About Programs, pp. 1–6. SIGPLAN 1, 1972.

    Google Scholar 

  48. R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

    Google Scholar 

  49. E. Moggi. An abstract view of programming languages. Technical Report ECSLFCS-90-113, University of Edinburgh, Comp. Sci. Dept., 1990.

    Google Scholar 

  50. E. Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991.

    Google Scholar 

  51. T. Nipkow and D. von Oheimb. Machine-checking the Java Specification: Proving Type-Saftey. In [5].

    Google Scholar 

  52. T. Nipkow and D. von Oheimb. Javalight is Type-Safe-Definitely. 25th ACM symposium on Principles of Programming Languages, 1998.

    Google Scholar 

  53. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Computer-Aided Verification (CAV’ 96), volume 1102 of LNCS, pages 411–414, New Brunswick, NJ, July/August 1996. Springer-Verlag.

    Google Scholar 

  54. B. Pierce and D. Turner. Concurrent objects in a process calculus. In Proceedings of TPPP’94. Springer LNCS 907, 1995.

    Google Scholar 

  55. A. Poetzsch-Heffter. Specification and verification of object-oriented programs. Technical report, Technical University of Munich, 1997. Habilitation Thesis.

    Google Scholar 

  56. A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In S.D. Swierstra, editor, Programming Languages and Systems (ESOP’ 99), volume 1576, pages 162–176. Springer-Verlag, 1999.

    Google Scholar 

  57. W. Pugh. Fixing the java memory model. In Java Grande, June 1999.

    Google Scholar 

  58. Z. Qian. Least Types for Memory Locations in Java Bytecode. Kestrel Institute, Tech Report, 1998.

    Google Scholar 

  59. A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.

    Google Scholar 

  60. A. Ruiz-Delgado, D. Pitt, and C. Smythe: A Review of Object-Oriented Approaches in Formal Specification. The Computer Journal, 38(10), 1995.

    Google Scholar 

  61. D. Syme. Proving Java Type Soundness. Technical report, University of Cambridge Computer Laboratory, 1997.

    Google Scholar 

  62. J. Wing. Writing Larch Interface Language Specifications. ACM Transactions on Programming Languages and Systems, 9(1):1–24, January 1987.

    Article  MATH  MathSciNet  Google Scholar 

  63. K. Yi and S. Ryu. Towards a cost-effective estimation of uncaught exceptions in SML programs. In Lecture Notes in Computer Science, volume 1302, pages 98–113. Springer-Verlag, proceedings of the 4th international static analysis symposium edition, 1997.

    Google Scholar 

  64. K. Yi and S. Ryu. SML/NJ Exception Analysis version 0.98. http://www.compiler.kaist.ac.kr/pub/exna/, December 1998.

Download references

Authors
  1. Bart Jacobs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gary T. Leavens
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Arnd Poetzsch-Heffter
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Informática Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa, 2825-114, Monte da Caparica, Portugal

    Ana Moreira

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jacobs, B., Leavens, G.T., Müller, P., Poetzsch-Heffter, A. (1999). Formal Techniques for Java Programs. In: Moreira, A. (eds) Object-Oriented Technology ECOOP’99 Workshop Reader. ECOOP 1999. Lecture Notes in Computer Science, vol 1743. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46589-8_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-46589-8_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66954-8

  • Online ISBN: 978-3-540-46589-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation