SRC Technical Note 1997-007
SRC Technical Note 1997-007When writing computer programs, programmers make assumptions about the relations among variables. In object-oriented programs, these assumptions include relations among the instance variables of a single object, relations often referred to as \emph{object invariants}. It is a good idea to explicitly annotate a program with these assumptions. Then, a static program-analysis tool can inspect the annotated program to check that routines preserve object invariants. This paper considers two issues that affect what object invariants a program analysis tool can check: object construction and modular checking. The paper suggests some programming idioms and program annotations that widen the range of object invariants that a static program checker can check. The paper also suggests a simple extension to the Java programming language that makes the language more amenable to object-invariant checking.
Back to the SRC Technical Notes main page.