Modular Specification of Frame Properties in JML

In: Concurrency and Computation: Practice and Experience. volume 15, p. 117--154, 2003

Authors

• Peter Müller
• Arnd Poetzsch-Heffter
• Gary T. Leavens

Abstract

We present a modular specification technique for frame properties. The technique uses modifies clauses and abstract fields with declared dependencies. Modularity is guaranteed by a programming model that enforces data abstraction by preventing representation and argument exposure, a semantics of modifies clauses that uses a notion of "relevant location", and by modularity rules for dependencies. For concreteness, we adapt this technique to the Java Modeling Language, JML.

BibTeX

@Article{Mueller.Poetzsch-Heffter.EA03modular, 
   author = {Peter Müller and Arnd Poetzsch-Heffter and Gary T. Leavens}
   title = {Modular Specification of Frame Properties in JML},
   journal = {Concurrency and Computation: Practice and Experience},
   publisher = {John Wiley & Sons, Ltd.},
   pages = {117--154},
   year = {2003},
}