Portal de Periódicos da CAPES

JML’s Rich, Inherited Specifications for Behavioral Subtypes

2006; Springer Science+Business Media; Linguagem: Inglês

10.1007/11901433_2

1611-3349

Gary T. Leavens,

Model-Driven Software Engineering Techniques

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.