In design by contract (DBC), assertions are typically written using program variables and query methods. This technique does not allow specifiers to write model-oriented specifications for interfaces in languages like Java. Moreover, 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. 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 solves all of the problems mentioned above. In addition, these features 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.