Transcript One Toolset for Design by Contract for Java

Static and Dynamic Contract Verifiers
For Java
Hongming Liu
Agenda



Introduction to Design by Contract.
Existing Design by Contract solutions.
Our Design by Contract toolset.
Design by Contract
http://archive.eiffel.com/doc/manuals/technology/contract/page.html


Design by Contract (DBC) theory suggests
associating a specification with every
software element. These specifications (or
contracts) govern the interaction of the
element with the rest of the world.
Component of a system communicate with
one another on the basis of precisely defined
benefits and obligations.
Design by Contract

Contract tags are specified as comments:


an example from the java.lang.String class:
/**
* @pre index >= 0
* @pre index < this.length()
*/
char charAt(int index){…}
Three types of basic contract tags:



Method preconditions.
Method postconditions.
Class invariants.
Design by Contract – Tags

Three tag types standard to DBC solutions:

Method precondition (@pre)


Method postcondition (@post)


a boolean expression assumed to be true whenever the
method is called.
a boolean expression assumed to be true when the
method returns.
Class invariant (@invariant)

a boolean expression that can assumed to be true in all
instances when the point of execution is not in a transit
state.
Design by Contract

Sets forth a system of obligations and
benefits.



The client has the obligation to satisfy the
preconditions of a method before calling that
method.
The supplier of the method has the obligation to
satisfy the postconditions of the method before
returning from that method.
Both receive the benefit of input or output values
that are guaranteed to comply to the contract.
Design by Contract – Tags

Three extended tags found in our DBC
solution:

Assert (@assert)


Fact (@fact)


assertion for a statement, equivalent to the
Java assert.
fact that is guaranteed to hold for a statement.
Loop invariant (@loopInvariant)

Invariant that holds for each iteration of a loop.
Design by Contract - Benefits
http://archive.eiffel.com/doc/manuals/technology/contract/page.html






Gives a better understanding of software
construction.
A systematic approach to building bug-free objectoriented systems.
A method for documenting software components.
An effective framework for debugging, testing, and
quality assurance.
Better understanding and control of the inheritance
mechanism.
A technique for dealing with abnormal cases, leading
to an effective language construct for exception
handling.
Design by Contract

Existing Tools include:




JDK 1.4 (assert)
iContract
JMSAssert
Eiffel
Our DBC Toolset

Components of our DBC Toolset:



DocGen – generates documentation (Javadoc) that
includes DBC information.
ContractChecker – creates modified versions of
Java classes with additional code that is used for
runtime checking of the contract.
Static Contract Verifier – statically checks Java
code for specific problems, such a possible nullpointer exceptions, array out of bounds
exceptions, or contract adherence at compile-time
(Static Contract Verification).
Our DBC Toolset

Advantages of our DBC Toolset:



Uses a specified syntax with high
expressiveness.
DocGen provides documentation that
includes contract information.
Static Analysis provides a partial alternative
to time-consuming runtime checking with
Static Analysis and Static Contract
Verification.
Static Contract Verification

Uses a weakest precondition algorithm.
/**
* weakest precondition: this.x >=1
* @pre this.x >= 2
* @post this’.x >= 0
*/
public void decrementX() {
this.x = this.x - 1;
}
Example – Contract
Generation
/**
* From a hypothetical Stack class.
* @pre this.size >= 1
* @post this'.size == this.size - 1
*/
public Object pop() {
Object e = this.stack[this.size - 1];
this.size = this.size - 1;
return e;
}
Generated Code - Part 1 of 2
public Object pop() {
if (!(this.size >= 1)) {
Contract contract =
Contract.getInstance();
contract.reportViolation(new
PreconditionException("PreconditionE
xception.occur
s:.the.precondition.contract.is.viol
ated:"));
}
Object e = this.stack[this.size - 1];
this.size = this.size - 1;
Object _$$_return = e;
Generated Code - Part 2 of 2
if (!(this.size == _pre$$_this.size - 1))
{
Contract contract =
Contract.getInstance();
contract.reportViolation(new
PostconditionException("Postconditio
nException.occ
urs:.the.postcondition.contract.is.v
iolated:"));
}
return _$$_return;
}
Miscellaneous



Thank you to Dr. Jia, Frank Qin, and
Jing Wang.
Project website is at:
http://se.cs.depaul.edu/ise/zoom/
Questions?