COMP2100/6442
Software Design Methodologies / Software Construction
Design by Contract (DbC) COMP2100/6442
Bernardo Pereira Nunes
Outline
▪ Overview ▪ Contract
▪ Interfaces
▪ A bit of history
▪ Design by Contract ▪ JML
▪Tools
2
What is a Contract?
A contract is a legally binding document that recognizes and governs the rights and duties of the parties to the agreement. A contract is legally enforceable because it meets the requirements and approval of the law.
A contract typically involves the exchange of goods, service, money, or promise of any of those. (and in Software Development?)
“Breach of contract”, means that the law will have to award the injured party either the access to legal remedies such as damages or cancellation. (Wikipedia)
(again, and in Software Development?)
3
Is an interface a contract?
Implementing an interface allows a class to become more formal about the behaviour it promises to provide.
Interfaces form a contract between the class and the outside world, and this contract is enforced at build time by the compiler.
If your class claims to implement an interface, all methods defined by that interface must appear in its source code before the class will successfully compile.
https://docs.oracle.com/javase/tutorial/java/concepts/interface.html
4
What is an Interface?
An interface is a contract that guarantees to a client how a class will
behave. When a class implements an interface, it tells any potential client:
“I guarantee I will support the methods, properties, events, and indexers of the named interface” .
https://www.oreilly.com/library/view/programming-c/0596001177/ch08.html
5
What is Design by Contract (DbC)?
…is a method for developing software!
Idea: a class and its clients have a contract with each
other.
Client: guarantees certain conditions before calling a method defined by a class (preconditions).
Class: guarantees certain properties that will hold after the call (postconditions).
A contract in software specifies both obligations and rights of clients and implementors.
6
A Bit of History – Design by Contract
Design by Contract is a trademarked term of Bertrand Meyer.
Many developers refer to it as Contract Programming. Bertrand developed DbC as part of the Eiffel Language.
Eiffel Language was conceived in 1985, is an object-oriented programming language and the main goal is to increase the reliability of software construction/development.
Many of the concepts introduced by Eiffel Language
were later adopted by other languages, for instance, Java.
Bertrand Meyer ETH Zurich
7
Basic Premise
“To improve software reliability, the first and perhaps most difficult problem is to define as precisely as possible, for each software element, what it is supposed to do”.
Associate a specification with every software element.
These specifications (or
contracts) govern the interaction of the element with the rest of the world.
Source: Wolfgang Pelz 2000-04 8
Benefits
A better understanding of the object-oriented method and, more generally, of software construction.
A systematic approach to building “bug-free” object-oriented systems. An effective framework for debugging, testing and, more generally,
quality assurance.
A method for documenting software components.
Better understanding and control of the inheritance mechanism.
A technique for dealing with abnormal cases, leading to a safe and effective language construct for exception handling.
Source: Wolfgang Pelz 2000-04 9
Example
Party
Client
Obligations
Provide letter or package of no more than 5 kgs, each dimension < 2 meters.
Pay 100 francs.
Deliver package to recipient in 4 hours or less.
Benefits
Get package delivered in 4 hours or less
UPS
No need to deal with deliveries too big,
too heavy, or unpaid.
Source: Wolfgang Pelz 2000-04 10
Example (explanation)
The idea of DbC is a metaphor on how elements of a software system collaborate with each other on the basis of mutual obligations and benefits.
The metaphor comes from business life, where a "client" and a "supplier" agree on a "contract" that defines, for example, that:
• The supplier must provide a certain product (obligation) and is entitled to expect that the client has paid its fee (benefit).
• The client must pay the fee (obligation) and is entitled to get the product (benefit).
Both parties must satisfy certain obligations, such as laws and regulations, applying to all contracts.
Source: Wikipedia
11
Concepts: Precondition
• Preconditions specify conditions that must hold before a method can execute. As such, they are evaluated just before a method executes. Preconditions involve the system state and the arguments passed into the method.
• Preconditions specify obligations that a client of a software component must meet before it may invoke a particular method of the component. If a precondition fails, a bug is in a software component's client.
https://www.infoworld.com/article/2074956/icontract-design-by-contract-in-java.html
12
Concepts: Postcondition
• Postconditions specify conditions that must hold after a method completes. Consequently, postconditions are executed after a method completes. Postconditions involve the old system state, the new system state, the method arguments, and the method's return value.
• Postconditions specify guarantees that a software component makes to its clients. If a postcondition is violated, the software component has a bug.
https://www.infoworld.com/article/2074956/icontract-design-by-contract-in-java.html
13
Concepts: Invariants
• An invariant specifies a condition that must hold anytime a client could invoke an object's method.
• Invariants are defined as part of a class definition. In practice, invariants are evaluated anytime before and after a method on any class instance executes. A violation of an invariant may indicate a bug in either the client or the software component.
https://www.infoworld.com/article/2074956/icontract-design-by-contract-in-java.html
14
Rationale
A contract document protects both the client, by
specifying how much should be done, and the supplier, by stating that the supplier is not liable for failing to carry out tasks outside of the specified scope.
The obligations of the supplier become the benefits to the client.
Source: Wolfgang Pelz 2000-04 15
Assertions (pre and postconditions)
routine_name (argument declarations) is require
Precondition do
Routine body (instructions) ensure
Postcondition end
Source: Wolfgang Pelz 2000-04 16
Violation of an Assertion
A precondition violation indicates a bug in the client (caller); the caller did not observe the conditions imposed on correct calls
A postcondition violation is a bug in the supplier (called routine); the routine failed to deliver on its promises
Source: Wolfgang Pelz 2000-04 17
Effect on Software
• strongpreconditions
– heavier burden on the client – lighter burden on the supplier
• dealingwithabnormalvaluesisapragmatic decision about division of labor
Source: Wolfgang Pelz 2000-04 18
Example
This is a contract for a sqrt method. It takes a number and returns its square root.
The static method approximatelyEqualTo of the class JMLDouble tests whether the relative difference of the first two double arguments is within the given epsilon, the third argument.
Obligation of the client: pass a positive number Client has the right to: obtain the square root approximation as the result
Obligation of the supplier: compute and return a square root approximation
Supplier can assume that it will receive a positive number
Clients are obliged to establish the precondition of each method called, but in return they are saved the trouble of achieving the postconditions themselves.
19
Tools
JML – Java Modelling Language http://www.jmlspecs.org/
iContract – Java Design by Contract Tool AssertMate – Java Design by Contract Tool
JASS – Java Design by Contract Tool http://semantik.informatik.uni-oldenburg.de/~jass/
C4J – Java Design by Contract Tool http://c4j.sourceforge.net
...
20
Java Modelling Language (JML)
Formal specification language for Java > to specify behaviour of Java classes
> to record design and implementation decisions by adding assertions to Java source code, e.g.,
preconditions • postconditions • invariants
The goal of JML is to be easy to use for any Java programmer
Source: Erik Poll | Radboud University Nijmegen
21
Java Modelling Language (JML)
To make JML easy to use and understand:
Properties can be specified as comments in .java source file:
/*@ . . . @*/
or
//@
*You can also use a separate file (.jml)
Properties are specified in Java syntax, namely as Java boolean expressions:
• extended with a few operators (\old, \forall, \result, … ).
• using a few keywords (requires, ensures, invariant, pure, non null, … )
Source: Erik Poll | Radboud University Nijmegen
22
Example JML Specification
public class IntegerSet {
byte[] a; /* The array a is sorted */ …
Source: Erik Poll | Radboud University Nijmegen
23
Example JML Specification
public class IntegerSet { …
byte[] a; /* The array a is sorted */
/*@ invariant
(\forall int i; 0 <= i && i < a.length-1; a[i] < a[i+1]);
@*/
...
Source: Erik Poll | Radboud University Nijmegen
24
Example JML Specification
Informal comment formal JML invariant
“The array a is sorted” (\forall int i; 0 <= i && i < a.length-1; a[i] < a[i+1])
They document the same property, but:
• JML spec has a precise meaning (e.g., < not <=) • Precise syntax and semantics allows tool support:
> runtime assertion checking: executing code and testing all assertions for a given set of inputs
• verification: proving that assertions are never violated, for all possible inputs
Source: Erik Poll | Radboud University Nijmegen
25
Running Example
public class BankAccount {
final static int MAX_BALANCE = 1000;
int balance;
int debit(int amount) {
balance = balance – amount;
return balance;
}
int credit(int amount) {
balance = balance + amount; return balance;
}
public int getBalance(){
return balance;
}
…
Source: Erik Poll | Radboud University Nijmegen
26
Requires
Precondition for method can be specified using requires:
/*@ requires amount >= 0; @*/ public int debit(int amount) {
…
}
Anyone calling the debit method has to guarantee the precondition.
Source: Erik Poll | Radboud University Nijmegen
27
Ensures
Postcondition for a method can be specified using ensures: /*@ requires amount >= 0;
ensures balance == \old(balance)-amount && \result == balance; @*/
public int debit(int amount) { …
}
Anyone calling the debit method can assume postcondition (if method terminates normally, i.e., does not throw exception)
\old(…) has obvious meaning
Source: Erik Poll | Radboud University Nijmegen
28
Design by Contract in JML
Pre and postcondition define a contract between a class and its clients: • Client must ensure precondition and may assume postcondition
• Method may assume precondition and must ensure postcondition
E.g., in the example specs for the debit method, it is the obligation of the client to ensure that amount is positive. The requires clause makes this explicit.
Source: Erik Poll | Radboud University Nijmegen
29
Requires and Ensures
JML specifications can be as strong or as weak as you want:
/*@ requires amount >= 0; ensures true; @*/
public int debit(int amount) { …
}
Default postcondition “ensures true” can be omitted. Idem for default precondition “requires true”.
(* text here *) JML treats informal description as a Boolean expression.
You can combine informal and formal descriptions (mainly when the formal statements are not easy/clear to write or expensive).
Source: Erik Poll | Radboud University Nijmegen
30
Invariants
Invariants (aka class invariants) are properties that must be maintained by all methods!
For example:
public class BankAccount {
final static int MAX_BALANCE = 1000; int balance;
/*@ invariant 0 <= balance && balance <= MAX_BALANCE; @*/ ...}
> Invariants are implicitly included in all pre and postconditions > Invariants must be preserved if exception is thrown!
> Invariants must be true at the end of constructor
> Invariants must be preserved by each method
> Invariants may be violated during the method execution
Source: Erik Poll | Radboud University Nijmegen
31
Nullable & Non_Null
/*@ non_null @*/ int[] a;
As most references are non-null, JML takes this as
default.
Only nullable fields need to be annotated, e.g.
/*@ nullable @*/ int[] b;
Default is non_null (!)
Source: Erik Poll | Radboud University Nijmegen
32
Pure (also called query methods)
Methods without side-effects that are guaranteed to terminate or throw an
exception can be declared as pure
:
/*@ pure @*/ int getBalance () {
return balance;
}
Pure methods can be used in JML annotations
:
//@ requires amount <= getBalance();
public void debit (int amount){
... }
*Java’s assignment expressions are not allowed (=, +=, -=, ..., --, ++). Only pure methods can be called in assertions.
33
Assignable
For non-pure methods, class properties can be modified using assignable clauses, for example:
/*@ requires amount >= 0 && balance >= amount; assignable balance;
ensures balance == \old(balance) – amount; @*/ public void debit(int amount){
… }
debit is only allowed to modify the balance field
34
Assignable
The default assignable clause is
//@ assignable \everything;
Pure methods are
//@ assignable \nothing;
Pure constructors are
//@ assignable this.*;
35
Multiple Clauses
Similarly for ensures, invariant: requires P;
requires Q;
is equivalent to:
requires P && Q;
36
Exceptions / signals
/*@ requires balance < amount;
@ signals (Exception) balance == \old(balance);
@ signals_only Exception; @ also
@ requires balance >= amount;
@ assignable balance;
@ ensures balance == \old(balance) – amount; @*/
public void debit(int amount) throws Exception { if (this.balance < amount) {
throw new Exception("Operation not supported”); } else {
this.balance -= amount; }
}
If the precondition does not hold, the method should throw exceptions.
signals specifies an exception and postconditions which should be satisfied when an exception occurs.
signals_only specifies an exception when the given precondition does not hold.
*The keyword also indicates that the method inherits specifications from superclasses.
37
DbC as Documentation[1]
It provides good documentation (classes and interfaces)
> For each method of a class or interface, the contract says what it requires, if
anything, from the client and what it ensures to the client > Better for documentation than just code
>> Even better than informal documentation (code comments or Javadoc)
> More abstract than code (does not implement the algorithm, focus only on what is
assumed and what must be achieved)
> Formal specification can be checked, comments cannot
> Increases the chances of being kept up-to-date with respect to the code (informal documentation is often outdated)
38
JML and OpenJML
JML annotations can be attached to Java programs by writing them directly into the Java source code files
JML annotations are ignored by JAVA (& JAVAC) JML needs a tool to verify JML statements: OpenJML
“OpenJML is a program verification tool for Java programs that allows you to check the specifications of programs annotated in JML”
Download & Installation:
https://www.openjml.org/documentation/installation.shtml
Note that OpenJML currently supports Java 8 (not 7 or 9) Example code – GitLab/Repo
39
Think about…
Design by Contract records details of methods responsibilities. It can be used for internally called methods to avoid constantly rechecking the validity of arguments. It can also be used to specify the effect of calling a method, and thus for recording details in a design. [1]
Which properties to specify?
Which level of detail?
Which tool should I use?
How expensive it can be? How to make it cost-effective? Which kind of projects should I use JML?
Is it the better way to document software?
40
Meme for today’s lecture! Keep practicing!
“My code was my documentation”, said a former developer.
41
Recommended Reading
JML reference manual
http://www.eecs.ucf.edu/~leavens/JML/refman/jmlrefman.pdf
General information
http://www.eecs.ucf.edu/~leavens/JML//index.shtml
42