Model Variables: Cleanly Supporting Abstraction in Design By Contract







Deposit Papers 


Cheon, Yoonsik, Leavens, Gary T., Sitaraman, Murali and Edwards, Stephen (2003) Model Variables: Cleanly Supporting Abstraction in Design By Contract. Technical Report TR #03-10, Department of Computer Science, Iowa State University.

Full text available as:Adobe PDF

There is a later version of this eprint available: Click here to view it.


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.

Keywords:documentation, formal methods, model variables, programming by contract, runtime assertion checking, specification languages, tools, Java language, JML language.
Subjects:Software: SOFTWARE ENGINEERING (K.6.3)
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Testing and Debugging
ID code:00000260
Deposited by:Yoonsik Cheon on 28 April 2003

Available Versions of This Paper

Contact site administrator at: