Contracts and Aspects
David H. Lorenz, Northeastern UniversityTherapon Skotiniotis, Northeastern University
Recently it has been shown that Design by Contract (DBC) in OOP have been erroneously enforced by existing DBC technologies. The crosscutting nature of DBC and its runtime enforcement, make it an ideal problem for AOSD to solve. In this paper we present an AOSD DBC tool, \conaj\, that provides DBC support by means of aspects, accommodating also pre- and post-conditions for advice. \conaj\ is based on the analysis of the relationships of pre- and post-conditions between aspects and their advised objects. Assertions on advice guarantees that addition of aspe cts honors the underlying systems obligations and does not break existing system behavior due to erroneous advice attachments or conflicting aspect--object obligations. AOSD development benefits as runtime error reporting becomes more accurate and advice expectations and obligations are now explicitly defined and validated. As a result increasing the ability to reason about composition as well as the behavior of aspects.
Technical Report NU-CCIS-03-13,
College of Computer and Information Science, Northeastern University, December 2003.
This research was partially supported by
the National Science Foundation under
award number CCR-0204432.
NU-CCIS-03-13.ps.gz (92k)
NU-CCIS-03-13.pdf (360k)
Implementation:
Cona is a preprocessing tool, generating AspectJ aspects for enforcing assertions.
Cona allows for the definitions of pre-, post-conditions
and invariants. Definitions are specified using
the syntax @pre{expr},
@post{expr},
@invariant{expr}. These can be placed
inside class as well as interface definitions. Invariant
definitions are allowed in the beginning or end of a
class/interface definition. Pre- and post-condition definitions
are allowed anywhere in the methods body, and after a methods
signature inside an interface definition.
An expr can be any valid java boolean expression,
extended with the definitions old to refer
to the state of an object prior to the a call to a method. Also
the usage of a methods name inside a post-condition is allowed
to refer to a non-void return value of the method.
Download:
Code examples:
- Stack example: MyStack.cona
- Console example: IConsole.cona; Console.cona; PrefixedConsole.cona; RunningConsole.cona; Main.java
The stack example in cona:
import java.util.Vector;
import java.util.Iterator;
import java.io.StringWriter;
class MyStack {
@invariant{ 0 <= size() && size() <= maxSize }
protected Vector elements;
protected int maxSize;
protected int size;
MyStack(int n){
elements = new Vector(n);
maxSize = n;
size = 0;
}
public int size() {
return size;
}
public void push(int i){
@pre{ !full() }
@post{ !empty() && top() == i && size() == old.size() + 1}
Integer val = new Integer(i);
elements.add(val);
size=elements.size();
}
public int pop(){
@pre{!empty()}
@post{!full() && size() == old.size() - 1}
Integer result = (Integer) elements.lastElement();
int index = elements.lastIndexOf(result);
elements.remove(index);
size = elements.size();
return result.intValue();
}
public int top(){
Integer result = (Integer) elements.lastElement();
return result.intValue();
}
public boolean full(){
return (size() == this.maxSize);
}
public boolean empty(){
return elements.isEmpty();
}
public String printMe(){
StringWriter sw = new StringWriter();
int index = 0;
Iterator it = elements.iterator();
while(it.hasNext()){
sw.write(" "+((Integer)it.next()).intValue()+" ");
index++;
}
return sw.toString();
}
}
The aspects genrated by Cona for the stack example:
privileged aspect MyStack_Contract {
declare parents : MyStack implements Cloneable;
public Object MyStack.clone() {
try {
return super.clone();
} catch (Exception e) {
/* Error */
}
}
MyStack old;
pointcut scope():
!within(MyStack_Contract)
&& !cflow(withincode(* MyStack_Contract.*(..)));
pointcut MyStack_push(MyStack trg_instance, int i):
call(public * MyStack.push(..))
&& !call(public * (MyStack+ && !MyStack).push(..))
&& args(i) && target(trg_instance) && scope();
pointcut dynamic_MyStack_push(MyStack trg_instance, int i):
execution(public * MyStack.push(..))
&& !execution(public * (MyStack+ && !MyStack).push(..))
&& args(i) && target(trg_instance) && scope();
// PCD for Invariant
pointcut MyStack_invariant(MyStack trg_instance):
call(public * MyStack.*(..))
&& !call(public * (MyStack+ && !MyStack).*(..))
&& target(trg_instance) && scope();
before(MyStack trg_instance):
MyStack_invariant(trg_instance){
if (!checkInvariant(trg_instance)) { /* Invariant Error */
System.out.println("error in inv before a method call");
System.exit(1);}
}
before(MyStack trg_instance, int i):
MyStack_push(trg_instance, i) {
old = (MyStack) trg_instance.clone();
boolean res = PreCond_push(trg_instance, i);
boolean next = true ;
if (!res) { /* PreCond Error */
System.out.println(" *** PRE CONDITION ERROR in MyStack in Method: push");
System.exit(1);
}
if (!next) { /* HierPreCond Error */
System.out.println(" *** PRE HIER ERROR in MyStack in Method: push");
System.exit(1);
}
}
before(MyStack trg_instance, int i):
dynamic_MyStack_push(trg_instance, i){
String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
String dynamicType = thisJoinPoint.getTarget().getClass().getName();/*]*/
boolean hierResult = (true);
boolean res = PreCond_push(trg_instance, i);
if (hierResult && ! res) { /* HierPreCond Error */
System.out.println(" **** CAST PRE HIER ERROR MyStack in Method: push");
System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" ****
dynamicType "+dynamicType+" SIG ==> "+
thisJoinPoint.getSignature().toLongString());System.exit(1);
}
}
after(MyStack trg_instance, int i):
MyStack_push(trg_instance, i) {
boolean res = PostCond_push(trg_instance, i);
if (!res) { /* PostCond Error */
System.out.println("Failed in post condition in: MyStack in Method: push");
System.out.println("Exiting ... ");
System.exit(1);
}
boolean postHier = PostCondHier_push(trg_instance, res,i);
if(!postHier){ /* HierPostCond Error */
System.out.println("Failed in post hier in: MyStack in Method: push ");
System.exit(1);
}
}
after(MyStack trg_instance, int i):
cast_MyStack_push(trg_instance, i){
boolean postResult = PostCond_push(trg_instance, i);
if(!postResult){ /* PostCond Error */
System.out.println("Failed in post condition in: MyStack in Method: push");
System.out.println("Exiting ... ");
System.exit(1);
}
boolean postHier = (true);
if(!postHier){ /* HierPostCond Error */
System.out.println("Failed in post hier in: MyStack in Method: push ");
String staticType = thisJoinPoint.getSignature().getDeclaringType().getName();
String dynamicType = thisJoinPoint.getTarget().getClass().getName();
System.out.println(" **** CAST POST HIER ERROR MyStack in Method: push");
System.out.println("[conaj-ERROR]: ***** staticType "+staticType+" ****
dynamicType "+dynamicType+" SIG ==> "+
thisJoinPoint.getSignature().toLongString());System.exit(1);
}
}
after(MyStack trg_instance):
MyStack_invariant(trg_instance){
if (!checkInvariant(trg_instance)){ /* Invariant Error */
System.out.println("error in inv after a method call");
System.exit(1);
}
}
public boolean checkInvariant(MyStack trg_instance){
if (0<=trg_instance.size()&&trg_instance.size()<=trg_instance.maxSize)
return true;
else
return false;
}
public boolean PreCond_push(MyStack trg_instance,int i){
if(!trg_instance.full())
return true;
else
return false;
}
public boolean PostCond_push(MyStack trg_instance,int i){
if(!trg_instance.empty() && trg_instance.top() == i && trg_instance.size() == old.size() + 1)
return true;
else
return false;
}
public boolean PreCondHier_push(MyStack trg_instance,int i){
boolean myPre = PreCond_push(trg_instance, i);
boolean hierarchy = (true);
if (!hierarchy || myPre)
return myPre;
else
return false;
}
public boolean PostCondHier_push(MyStack trg_instance, boolean last,int i){
boolean postResult = PostCond_push(trg_instance, i);
if (!last || postResult)
return (true);
else
return false;
}
}
@TechReport{Lorenz:2003:CAA,
Title = {Contracts and Aspects},
Author = {David~H. Lorenz and Therapon Skotiniotis},
Number = "{NU-CCIS-03-13}",
Institution = "College of Computer and Information Science, Northeastern University",
Address = "Boston, MA 02115",
Month = dec,
Year = 2003,
URL = "\url{http://www.ccs.neu.edu/home/lorenz/papers/reports/NU-CCIS-03-13.html}",
}