Publication Date

8-11-2006

Technical Report Number

TR06-22

Subjects

Computer Systems Organization, Software, Theory of Computation

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.

Comments

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

Share

COinS