Publication Date

4-2001

Technical Report Number

TR01-03

Subjects

Software, Theory of Computation

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 restricts aliasing, and by modularity requirements for dependencies. For concreteness, we adapt this technique to the Java Modeling Language, JML.

Share

COinS