A Methodology for Invariants, Framing, and Subtyping in JML
- ,
- Gary T. Leavens(corresponding author)
- Pennsylvania State University,
- University of Central Florida
Scholary Output:
Chapter in Book/Report/Conference proceeding
Chapter
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.
Publication Information
Output type
Scholary Output:
Chapter in Book/Report/Conference proceeding
Chapter
Host publication Subtitle
Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th BirthdayOriginal language
English (US)Pages from-to (Number of pages)
Pages 19-39 (21 pages)Publication milestones
- Published - 01/01/2018
Publication status
Published - 01/01/2018
Publisher
Springer International PublishingISBN (Print)
9783319980461ISBN (Electronic)
9783319980478Publication IDs
- Scopus: 85115867388
Host publication title
Principled Software DevelopmentPublication metrics
Metrics
Fractional count
1
Fractional count
0.50
Fractional count
1
Fractional count
0.50
Fractional count
1
Fractional count
1
PlumX, opens in new tab
Citation count
2