Tools for Design By Contract


Design By Contract (DBC) is a systematic approach to specifying and implementing object-oriented software systems. DBC has been proved to greatly benefit software development. However, Java does not natively support DBC. We have developed a comprehensive solution to bring DBC into Java. The static and dynamic contract verifier is the most crucial part of the solution. We have developed a toolset support DBC using these two verifiers. The tool used for dynamic contract verifier is ContractChecker, which generates test code into original Java code, thus enables runtime validation. Static contract verification is done by Static Contract Verifier, which uses an automated theorem prover to verify contract.

Introduction

Design by Contract(DBC) was first introduced by Bertrand Meyer as part of the Eiffel Project. Under the DBC theory, a software system is viewed as a set of communicating components whose interaction is based on precisely defined specifications of the mutual obligations: contracts. DBC provides a formal way to incorporate specification information, which is obtained from comments, into the code. By doing this, the code’s implicit contracts are transformed into explicit requirements that must be satisfied.

DBC can be viewed as a systematic approach to specifying and implementing object-oriented software systems. Meyer enumerates the primary benefits of this approach:
  • A better understanding of object-oriented software construction in general
  • A systematic approach to building correct software systems
  • An effective framework for quality assurance
  • A method for documenting software
  • Better control of the inheritance mechanism
  • A technique for dealing with abnormal cases, leading to a proper use of exception handling mechanisms


The three key elements of DBC are method preconditions, method postconditions and class invariant. Method preconditions are conditions that the client must meet before a method is invoked. Method postcondtions are conditions that a method must meet after its execution. Class invariant are consistency conditions of objects, which must hold for all instances.

Java itself does not support DBC, though the assert statement introduced in JDK 1.4 does represent a step in this direction. Assert provides a mean for programmers to provide runtime checking for their programs. Assert, however, does not provide contract information to indicate the functionality of a method or class such as method preconditions, postconditions and class invariant, which are emphasized by DBC.

We present techniques for both static and dynamic contract verification, which is the key part of a comprehensive solution for bringing DBC into Java. Our static contract verification technique is theorem proving based. The theorem prover helps in evaluating the implications of conditions defined in the program. The dynamic contract verification is implemented by generating test code into original Java code, therefore enables runtime validation.

Overview of DBC Toolset Components

To demonstrate our solution for bringing DBC into java, we develop a DBC toolset, which is designed to incorporate DBC capability into the Java language, not only providing the conventions for DBC specification, but also consisting of three major components: ContractChecker, Static Contract Verifier and DocGen, which are intended to make use of the DBC information in the programs. Figure 1 shows the overview of these components.

           

Figure 1: Components of Our DBC toolset


ContractChecker does runtime checking for the contracts by generating new pieces of code and inserting them into the original code, so when executing the new code, any violations against the contract information programmer provide will be reported and avoid further severe exceptions.

Static Contract Verifier statically analyzes the program for potential null pointer and array out of bounds exceptions and also incorporates contract verification for each Java class and method. Contract verification indicates whether a specific method is able to satisfy the postconditions if the method’s preconditions are assumed to be true. If the postconditions are not guaranteed given satisfied preconditions the contract is invalid.

DocGen is a Java doclet developed on the basis of the standard doclet. It is able to extract and display any contract, including any inherited contract that is documented in a formal comment unit, as long as the documentation follows a certain format. DocGen has several major features that make it different from other similar tools: 1) It is based on the newest version of Java doclet, 2) It automatically processes all inherited contracts; 3) It allows some degree of flexibility in terms of where the contract should be documented.