"Specifying the modification of extended state"
K. Rustan M. Leino
Note #1997-026. October 30, 1997.

This paper explores the interpretation of specifications in the
context of an object-oriented programming language with subclassing
and method overrides, for example like Java.  In particular, the paper
considers annotations for describing what variables a method may
change and the interpretation of these annotations.  The paper shows
that there is a problem to be solved in the specification of methods
whose overrides may modify additional state introduced in
subclasses.  As a solution to this problem, the paper introduces
<I>data groups</I>, which enable modular checking and rather
naturally capture a programmer's design decisions.