Publication Date

10-2002

Technical Report Number

TR02-02a

Subjects

Software

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.

Share

COinS