Abstract
This paper explores the interpretation of specifications in the
context of an object-oriented programming language with subclassing
and method overrides. 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 data groups, which
enable modular checking and rather naturally capture a programmer's
design decisions.