Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

Formal Semantics for the Java Modeling Language

Reviewed Paper In Proceedings

Author(s):Daniel Bruns
In:Informatiktage 2010
Publisher:Gesellschaft für Informatik
Series:Lecture Notes in Informatics
Volume:S-9
Year:2010
Pages:15-18
URL:http://subs.emis.de/LNI/Seminar/Seminar09/S-09.pdf

Abstract

A common critique of formal methods in software development practise is, that they are not readily understandable and thus not widely used. The Java Modeling Language (JML) was created in an attempt to bridge that gap. By building upon the syntax of Java it is meant to be easily accessible to the common user – who might not be skilled in formal modeling. Due to this advantage, JML has quickly become one of most popular specification languages to use with both static and runtime analysis of programs. JML specifications are written in a Java-like expression language as comments straight into source files. It provides both in-code assertions as well as method contracts and class invariants which are indicated by appropriate preceding keywords. However, the official reference mostly lacks a clear definition of semantics. In turn, several tools implementing JML syntax use their own interpretations. Past approaches to formal semantics have rather been documentations of those tools than providing a unified reference.

Note

Best Paper Award

BibTeX

@InProceedings{Bruns10,
  author	= {Daniel Bruns},
  title		= {Formal Semantics for the {Java} {Modeling} {Language}},
  note		= {Best Paper Award},
  year		= 2010,
  month		= mar,
  booktitle	= {Informatiktage 2010},
  address	= {Bonn, Germany},
  pages		= {15--18},
  publisher	= {Gesellschaft f{\"u}r Informatik},
  series	= {Lecture Notes in Informatics},
  volume	= {S-9},
  isbn		= {978-3-88579-443-1},
  url		= {http://subs.emis.de/LNI/Seminar/Seminar09/S-09.pdf},
  language	= {english},
  abstract	= {A common critique of formal methods in software
		   development practise is, that they are not readily
		   understandable and thus not widely used. The Java Modeling
		   Language (JML) was created in an attempt to bridge that
		   gap. By building upon the syntax of Java it is meant to be
		   easily accessible to the common user -- who might not be
		   skilled in formal modeling. Due to this advantage, JML has
		   quickly become one of most popular specification languages
		   to use with both static and runtime analysis of programs.
		   JML specifications are written in a Java-like expression
		   language as comments straight into source files. It
		   provides both in-code assertions as well as method
		   contracts and class invariants which are indicated by
		   appropriate preceding keywords. However, the official
		   reference mostly lacks a clear definition of semantics. In
		   turn, several tools implementing JML syntax use their own
		   interpretations. Past approaches to formal semantics have
		   rather been documentations of those tools than providing a
		   unified reference.}
}