Programming by Contract

Student: Alicia Rohrberg

Topic: Design by Contract (known often as Programming by Contract)

Email: arohrber@calpoly.edu

Key Points:

• What it is and Why should you do it
• How do you do "Programming by Contract"
• Preconditions
• Postconditions
• Assertions
• Class Invariants
• Exceptions in the Contract

Presentation

What is Programming by Contract

Programming by Contract is a software correctness methodology. By using pre and post conditions, you can document the change in state caused by that piece of the program. Originally proposed by Bertrand Meyer who is the pioneering designer of the programming language, Eiffel. Methods are viewed as a way to fulfill a contract.

Benefits of Programming by Contract

• Better understanding of the object-oriented method
• Systematic approach to building bug-free object-oriented systems
• Effect framework for debugging, testing, and quality assurance
• Method for documenting software components
• Technique for dealing with abnormal cases

Doing Programming by Contract

When a developer is following "Programming by Contract" the following questions must constantly be asked ...

• What does it expect?
• What does it guarantee?
• What does it maintain?

Using Preconditions

• A precondition of a method is a condition that must be true before the method can be used.
• This fufills the question of "What does it expect?". When using a precondition, the method knows what to expect before the method is actually used.
• If the precondition is not met and the method is still called, the provider may chose any action.

Using Postconditions

• A postcondition of a method is a condition that is guaranteed to be true upon completion.
• This fulfills the questions of "What does the method guarantee?". A postcondition should state what the method guarantees to complete after the method call is completed.
• If the postcondition is not true after the method is called, an exception should not be thrown. The code should be modified by the developer such that the postcondition is true. Using assertions in the method can help verify the method does what it should.

Using Assertions

• An assertion is a condition that a programmer expects to be true.
• If an assertion passes, execution continues. If an assertion fails, then an error is thrown and the program usually terminates.
• Very helpful to use during testing to verify what the programmer thinks is happening
• Using assertions to verify a postcondition will help to guarantee the postcondition is true after the method is executed.
• After testing, assertions can be disabled (if the programmer wishes) so that the program will execute quicker.

Using Class Invariants

• A class invariant is a logical condition that holds for all objects of a class. (This may not be true in mutation)
• To prove an invariant ...
• check that it is true after every constructor is executed
• check that it is true before a mutator and true after it has executed

Exceptions in the Contract

• Does not require that a method never throws an exception.
• Often times to fulfill a contract an exception must be thrown.
• Certain preconditions are not verifiable and therefore an exception could be thrown. (File not found)

Exam Questions

Question #1. What are the three central ideas of Programming by Contract?

Solution #1: Preconditions, Postconditions (assertions), and Class Invariants

Question #2: What should you do if a postcondition fails?

Solution #2: Go back through your testing phases and use assertions to find where the method is failing. Once the assertion passes the postcondition will pass.

References:

• Horstmann's Object-Oriented Design and Patterns (3.6)
• http://www.eiffel.com/developers/knowledgebase/design_by_contract.html
• http://c2.com/cgi/wiki?DesignByContract