A Methodology for Invariants, Framing, and Subtyping in JML

Yuyan Bao; Gary T. Leavens

doi:10.1007/978-3-319-98047-8_2

A Methodology for Invariants, Framing, and Subtyping in JML

Yuyan Bao
, Gary T. Leavens

Research output: Chapter in Book/Report/Conference proceeding › Chapter

2 Scopus citations

Abstract

The Java Modeling Language (JML) is a specification language for describing the functional behavior of sequential Java program modules. The objectoriented features of Java make specifying invariants and framing difficult in the presence of subtyping. Using regions as a basis for a methodology, we precisely describe a technique for specifying invariants and framing in the presence of subtyping.We also extend JML by adding separating conjunction (from separation logic) for certain kinds of assertions.

Original language	English (US)
Title of host publication	Principled Software Development
Subtitle of host publication	Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday
Publisher	Springer International Publishing
Pages	19-39
Number of pages	21
ISBN (Electronic)	9783319980478
ISBN (Print)	9783319980461
DOIs	https://doi.org/10.1007/978-3-319-98047-8_2
State	Published - Jan 1 2018
Externally published	Yes

ASJC Scopus subject areas

General Computer Science
General Mathematics

Access to Document

10.1007/978-3-319-98047-8_2

Cite this

@inbook{23f213c3639f4c76887015296f22a6e3,

title = "A Methodology for Invariants, Framing, and Subtyping in JML",

abstract = "The Java Modeling Language (JML) is a specification language for describing the functional behavior of sequential Java program modules. The objectoriented features of Java make specifying invariants and framing difficult in the presence of subtyping. Using regions as a basis for a methodology, we precisely describe a technique for specifying invariants and framing in the presence of subtyping.We also extend JML by adding separating conjunction (from separation logic) for certain kinds of assertions.",

author = "Yuyan Bao and Leavens, \{Gary T.\}",

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2018.",

year = "2018",

month = jan,

day = "1",

doi = "10.1007/978-3-319-98047-8\_2",

language = "English (US)",

isbn = "9783319980461",

pages = "19--39",

booktitle = "Principled Software Development",

publisher = "Springer International Publishing",

}

TY - CHAP

T1 - A Methodology for Invariants, Framing, and Subtyping in JML

AU - Bao, Yuyan

AU - Leavens, Gary T.

N1 - Publisher Copyright: © Springer Nature Switzerland AG 2018.

PY - 2018/1/1

Y1 - 2018/1/1

N2 - The Java Modeling Language (JML) is a specification language for describing the functional behavior of sequential Java program modules. The objectoriented features of Java make specifying invariants and framing difficult in the presence of subtyping. Using regions as a basis for a methodology, we precisely describe a technique for specifying invariants and framing in the presence of subtyping.We also extend JML by adding separating conjunction (from separation logic) for certain kinds of assertions.

AB - The Java Modeling Language (JML) is a specification language for describing the functional behavior of sequential Java program modules. The objectoriented features of Java make specifying invariants and framing difficult in the presence of subtyping. Using regions as a basis for a methodology, we precisely describe a technique for specifying invariants and framing in the presence of subtyping.We also extend JML by adding separating conjunction (from separation logic) for certain kinds of assertions.

UR - https://www.scopus.com/pages/publications/85115867388

UR - https://www.scopus.com/pages/publications/85115867388#tab=citedBy

U2 - 10.1007/978-3-319-98047-8_2

DO - 10.1007/978-3-319-98047-8_2

M3 - Chapter

AN - SCOPUS:85115867388

SN - 9783319980461

SP - 19

EP - 39

BT - Principled Software Development

PB - Springer International Publishing

ER -

A Methodology for Invariants, Framing, and Subtyping in JML

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this