Title

Tutorial On Jml, The Java Modeling Language

Keywords

assertion; behavioral subtype; design by contract; extended static checking; information hiding; invariant; java modeling language (JML); model field; runtime assertion checking; specification; specification inheritance; tool; verification

Abstract

The Java Modeling Language (JML) is widely used in academic research as a common language for formal methods tools that work with Java. JML is a design by contract language that can be used to specify detailed designs of Java programs, frameworks, and class libraries. Over twenty research groups worldwide have built several tools for checking code and finding bugs (see jmlspecs.org). This tutorial will give background for researchers and practitioners interested in doing formal methods research and in using JML for specifying the sequential behavior of Java classes and interfaces. Attendees will write JML specifications for a data type, including pre- and postconditions for methods and object invariants. They will also learn how to use the most important JML tools. In addition, they will learn how to use model fields to hide the actual field declarations in classes, and how JML supports modular reasoning about subtypes with behavioral subtyping.

Publication Date

12-1-2007

Publication Title

ASE'07 - 2007 ACM/IEEE International Conference on Automated Software Engineering

Number of Pages

573-

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1145/1321631.1321747

Socpus ID

77954025695 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/77954025695

This document is currently not available here.

Share

COinS