Model Variables: Cleanly Supporting Abstraction 
			in Design By Contract

		   Yoonsik Cheon, Gary T. Leavens,
		Murali Sitaraman, and Stephen Edwards

			       Abstract

In design by contract (DBC), assertions are typically written using
program variables and query methods.  The lack of separation between
program code and assertions is confusing, because readers do not know
what code is intended for use in the program and what code is only
intended for specification purposes.  This lack of separation also
creates a potential runtime performance penalty, even when runtime
assertion checks are disabled, due to both the increased memory
footprint of the program and the execution of code maintaining that
part of the program's state intended for use in specifications.  To
solve these problems, we present a new way of writing and checking DBC
assertions without directly referring to concrete program states,
using ``model'', i.e., specification-only, variables and methods.  The
use of model variables and methods does not incur the problems
mentioned above, but it also allow one to write more easily assertions
that are abstract, concise, and independent of representation details,
and hence more readable and maintainable.  We implemented these
features in the runtime assertion checker for the Java Modeling
Language (JML), but the approach could also be implemented in other
DBC tools.

Keywords: assertions, model variables, runtime assertion checking,
  design by contract, Java language, JML language.

2001 CR Categories: 
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, tools, JML;
D.2.2 [Software Engineering]
        Design Tools and Techniques --- modules and interfaces,
        object-oriented design methods;
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers,
        class invariants, correctness proofs, formal methods,
        programming by contract, reliability, tools, validation, JML;
D.3.2 [Programming Languages]
	Language Classifications --- Object-oriented languages;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
        Assertions, invariants, logics of programs, mechanical
        verification, pre- and post-conditions, specification techniques;

Copyright (c) 2003 Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman,
and  Stephen Edwards.