JML's Rich, Inherited Specifications for Behavioral Subtypes

Date
2006-08-11
Authors
Leavens, Gary
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

The Java Modeling Language (JML) is used to specify detailed designs for Java classes and interfaces. It has a particularly rich set of features for specifying methods. This paper describes those features, with particular emphasis on the features related to specification inheritance. It shows how specification inheritance in JML forces behavioral subtyping, through a discussion of semantics and examples. It also describes a notion of modular reasoning based on static type information, supertype abstraction, which is made valid in JML by methodological restrictions on invariants, history constraints, and initially clauses and by behavioral subtyping.

Description

Copyright © 2006, Springer-Verlag.

This is a preprint of an Invited talk to appear in Zhiming Liu and He Jifeng (eds), Proceedings, International Conference on Formal Engineering Methods (ICFEM'06), Macao, China}, pages 2-36. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006

Keywords
Supertype abstraction, behavioral subtype, behavioral subtyping, modularity, specification inheritance, method specification refinement, join of method specifications, also, specification case, invariants, JML, Java
Citation
DOI
Source
Collections