Transcript Design by Contract in Java

Design by Contract in Java
Concept and Comparison
What is DBC?

Classes of a system communicate
with one another on the basis of
precisely defined benefits and
obligations.
[Bertrand Meyer, CACM, Vol. 36, No 9,
1992]
What is DBC? (cont.)

Preconditions of methods
A boolean expression which is assumed true when the
method gets called

Postconditions of methods
A boolean expression which the caller can assume to be
true when the method returns

Class invariants
consistency conditions of objects
must hold for all instances
Preconditions, Postconditions and
Class Invariants
/**
* @invariant gpa >= 0
*/
class Student {
protected _gpa;
/**
* GPA always >=0
* @pre gpa >= 0
*/
void setGPA (double gpa){…}
/**
* GPA always >=0
* @post return >= 0
*/
double getGPA(){…}
}



@pre
@post
@invariant
Preconditions, Postconditions
and Class Invariants (cont.)
http://archive.eifel.com/doc/manuals/technology/contract/pafe.html
e.g., inserting a certain element into a dictionary
(a table where each element is identified
by a certain character string used as key) of bounded capacity.
put (x: ELEMENT; key: STRING) is
-- Insert x so that it will be retrievable through key.
require
count <= capacity
not key.empty
do
... Some insertion algorithm ...
ensure
has (x)
item (key) = x
count = old count + 1
end
The Notion of Contract
http://archive.eifel.com/doc/manuals/technology/contract/pafe.html
Client
Supplier
 Obligations
(Must ensure precondition)
 Benefits
(May benefit from postcondition)
Make sure table is not
full and key is a nonempty string.
Get updated table where the
given element now
appears, associated with
the given key.
(Must ensure postcondition)
(May assume precondition)
Record given element in
table, associated with
given key.
No need to do anything if
table is full, or key is
empty string.
The Notion of Contract (cont.)
http://archive.eifel.com/doc/manuals/technology/contract/pafe.html
Client

Obligations


Satisfy preconditions


Supplier

Satisfy postconditions


Benefits
No need to check output
values
Result guaranteed to
comply to postcondition
No need to check input
values
Input guaranteed to
comply to precondition
Benefits of Design by Contract






Better understanding of software construction
Systematic approach to building bug-free oo
systems
Effective framework for debugging, testing and
quality assurance
Method for documenting software components
Better control of the inheritance mechanism
Technique for dealing with abnormal cases,
effective exception handling
Current Existing Tools

Formal documentation
informal, implicit vs. formal, explicit

Runtime validation
translate the contract into runtime assertions
most common

Static analysis
use model checking, theorem prover to analyze at compile
time
Current Existing Tools (cont.)


JDK1.4: assert
Eiffel
http://archive.eiffel.com

iContract
by Reto Kramer, Cambridge Technology Partners

JASS
http://semantik.informatik.uni-oldenburg.de/~jass/

JMSAssert
by man machine systems
http://www.mmsindia.com/JMSAssert.html

Jtest and Jcontract
by parasoft
http://www.parasoft.com
What are These Tools For?



Most are runtime validation and
formal documentation
programmer-provided assertions
into source code, using a
preprocessor
At runtime, check if these
assertions are violated—possibly,
throw exceptions
What are These Tools For? (cont.)



Requirement: programmer needs to write
assertions (preconditions, postconditions,
class invariants) in certain documentation
format.
Run the preprocessors (possibly with
options) to get the instrumented
program.
Result: avoidance of any runtime
exceptions due to violation of assertions
(but still throw other exceptions).
Comparison Between These Tools
Expressive
ness
JDK1.4
iContract
My Tool
Usability
Runtime
Check
Static
Analysis
Low, not
specific
Low level
feature
Yes
No
Specified
contract
Tool with
multiple
features
Yes
No
Specified
contract
Tool with
multiple
features
Yes
Has
interface to
integrate
with static
error
checker
Comparison Between These Tools
(cont.)





How expressiveness?
How to deal with class hierarchies?
Other design issues
Implementation issues
Additional features
How Expressivness?
 JDK1.4:
low level features. dose not specify precondition,
postconditon and invariant
 Other
tools:
---preconditions, postconditions and invariants to be
checked at different entry of the program
---some have quantifiers: forall, exists, implies
---value at entry level of a method vs. value at return level
of a method
How Expressiveness? (cont.)

Forall (iContract):
forall <Class> <var> in <Enum> | <Expr_var>

Exists (iContract):
exists <Class> <var> in <Enum> | <Expr_var>

implies (iContract):
C implies I
e.g., each employee must be on the employment-list of all it’s employers:
@invariant employees_ != null
implies
forall Emplyee e in employees_.elements() |
exists Employer c in e.getEmployers() |
c == this
How Expressiveness? (cont.)

Old value, @pre (iContract):
@post this.size()==this.size()@pre + 1

Old value, $prev (JMSAssert):
@post a == $prev(a) + val
Class Hierarchies
(Class extension, interface implementation, interface extension and
innerclasses)

Why?
type, syntax vs. semantic
more strict on what a subtype should do

Example
interface human{
object getFood();
}
class cat implements human{
// might return raw rat, if no contract is made here
public object getFood() {…}
}
Class Hierarchies(cont.)


JDK1.4: No.
Eiffel:
--OR in precondition, AND in postcondition

iContract, JMSAssert:
--invariants: conjuncted (stronger in subtype)
--postconditions: conjuncted (stronger in
subtype)
--preconditions: disjuncted (weaker in
subtype)

JASS:
--must implement the interface
jass.runtime.refinement
Class Hierarchies (cont.)

Examples (JMSAssert)
class ImpEmployee implements Employee {
protected int eage;
interface Employee {
/**
* @post return > 25
*/
int getAge();
/**
* @post return < 65
*/
public int getAge(){
return age_;
}
/**
* @pre age > 25
*/
void setAge( int age);
/**
* @pre age < 65
*/
public void setAge( int age) {
eage = age;
}
…
}
}
Subclass can choose to deal with more conditions, but must offer at least the same service.
Other Design Issues
 How
to avoid non-terminating
recursion?
--iContract: keeps track of the call-chain at runtime
to prevent recursive non-termination checks.
--JASS: assertion is not checked at the first level of
internal calls. Beyond that, no restriction.
--JMSAssert: no specified.
Other Design Issues (cont.)

Example of recursive calls:
1: /**Example that demonstrates the automatic avoidance of
2: * recursive, non-terminating invariant checks
3: *
4: * @invariant forall Employee employee
5: *
in this.getEmployees().elements() |
6: *
employee.getEmployer() == this
7: */
8: class Employer {
9:
10: public static void main(String arv[]) {
11: Employer company = new Employer();
12: Employee george = new Employee();
13: company.add( george );
14: }
Other Design Issues (cont.)

Example of recursive calls (cont.):
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
protected Vector employees_ = new Vector();
Enumeration getEmployees() {
return employees_.elements();
}
void add(Employee employee) {
employee.setEmployer( this );
employees_.addElement( employee );
}
}
...
Other Design Issues (cont.)

Solution to prevent non-terminating
recursive calls (iContract)
/**
* @invariant age_ > 0
*/
public class Employee implements Person {
//#*#--------------------------------------------------------------private java.util.Hashtable __icl_ = new java.util.Hashtable();
private synchronized void __inv_check_at_entry__Employee(
Other Design Issues (cont.)

Solution to prevent non-terminating recursive calls
(iContract), cont.
Thread thread, String loc) {
if ( !__icl_.containsKey(thread) ) { // recursion depth 0
__icl_.put(thread, new Integer(1));
__check_invariant____Employee(loc); // evaluates the invariant
}
else // inc recursion depth
__icl_.put(thread, new Integer(
((Integer)__icl_.get(thread)).intValue()+1));
}
//#*#-----------------------------------------------------------------
Implementation Issues
 Performance
tuning
compile options to specify how strict the
assertion check is.
e.g., iContract:
java iContract.Tool –mpre,post,inv C.java >
C_instr.java
Additional Features

iContract:
Binary contract repositories: compiled
contract to be included in the distribution.

Jtest and Jcontract:
Test tool implementing design by
contract.
Main Features of My Tool
 Formal
documentation
 Better expressiveness
@pre, @post, @invariant, forall, exists,
implies, x’
 Compatible
with Java 1.4
 Runtime validation
 Interface with the static
analysis tool
Current Status

Done:
--javadoc that supports @pre, @post, @invariant,
etc.
--grammar for blocks of comment that are in certain
format, in .jjt form (using JavaCC):
e.g., @pre: a!=0&&b<0

To be done:
--incorporate the grammar for comment into the
AST of the whole program.
--instrumentation of the assertions