Jose: aspects for design by contract

Jose: Aspects for Design by Contract Yishai A. Feldman Efi Arazi School of Computer Science The Interdisciplinary Center, Herzliya [email protected]

Ohad Barzilay School of Computer Science Tel Aviv University [email protected]

Abstract Design by contract is a practical methodology for evolving code together with its specification. The contract has important methodological implications on the design of the program. In addition, tools that instrument the code to check for contract violations help the development process by catching errors close to their sources. This is complicated by several factors, such as the need to collect preconditions from supertypes. There are two issues involved in the implementation of such a tool: the correct enforcement of the theoretical principles, and the instrumentation of the code. Most previous tools tackle both issues, but have subtle failures in one or the other. This paper describes Jose, a tool for design by contract in Java, which uses AspectJ, an aspect-oriented extension of Java, to instrument the program. This allows us to leverage the expertise of the AspectJ developers in instrumenting Java programs, and concentrate on the correct implementation of the designby-contract principles. This approach has the added benefit that it can be generalized to other object-oriented languages that have aspect-oriented extensions. We describe the design decisions made in the implementation of Jose, and the features of AspectJ that helped or hindered this implementation.

1 Introduction The design-by-contract methodology [14] is used to distribute responsibility between a class and its users. The contract comprises three types of assertions: method pre- and postconditions and class invariants. Clients may only call methods when their preconditions are satisfied; in those cases, the supplier must make sure that postconditions are This research was supported in part by a grant from the Israel Science Foundation (grant No. 1011/04).

Shmuel Tyszberowicz School of Computer Science The Academic College of Tel Aviv Yaffo [email protected]

satisfied on exit from the method. Invariants define correct states for objects belonging to the class. The contract has important methodological implications for inheritance. According to the behavioral subtyping principle [10], subtypes may only weaken preconditions and strengthen postconditions and invariants. It is important to note that the principle is in effect whether or not programmers use design by contract. If contracts are not explicit, such bugs will be more frequenent than otherwise. Design by contract is directly supported by the Eiffel programming language [13]. The methodology is, of course, applicable to other object-oriented languages as well, and is useful even without tool support. Still, programmers who specify contracts for their classes naturally want the benefit of a tool that instruments their programs by adding code that checks for contract violations. This is very useful for the early discovery of errors. Such a tool must also enforce the behavioral subtyping principle. This means that the instrumentation code of one class depends on the contracts of other classes. In addition, postconditions need to be able to refer to the values of expressions at the beginning of the method call. For example, a method that adds an element to a data structure will have a postcondition like count() == $prev(count()) + 1, where the expression $prev(exp) refers to the value of exp on entry to the method. (This is called an old value, and some tools use the keyword old to denote such values.) The instrumented code needs to save the value of the expression before the method body executes, then use that value when checking the postcondition. The implementation of a design-by-contract tool therefore involves two separate issues. The first is the determination of what code needs to be inserted into the source program for the correct enforcement of the theoretical principles, and the second is the actual instrumentation of the program. Code instrumentation involves many issues such as the order of execution, dynamic dispatching, object initialization, inheritance, interface implementation, and oth-

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

ers. All of these are very technical and tightly coupled to the semantics and sometimes even the implementation of the underlying programming language. There are several design-by-contract tools for Java [1, 2, 4, 8, 11, 12, 15, 16], ranging from academic proofs-ofconcept to commercial systems. Most tackle both issues, and as a result have subtle problems with one or the other. (More details appear in Section 4.) We have implemented a system, called Jose,1 which relies on AspectJ [9] for the instrumentation of the program. This allows us to leverage the expertise of the AspectJ developers in instrumenting Java programs, and concentrate on the correct implementation of the design-by-contract principles. We describe the design decisions made in the implementation of Jose, and the features of AspectJ that help or hinder this implementation.

2 Design By Contract in Java There are several issues that complicate the correct implementation of contract assertions in Java. The most significant are discussed in this section.

2.1 Collecting Assertions from Supertypes There are two ways to enforce the behavioral subtyping principle. One is to check that whenever the precondition of a method in a subclass is false, so is the precondition of its superclass, and whenever the postcondition of a method in the subclass is true, so is the postcondition in the superclass [6]. The approach taken in Eiffel, and in most design-bycontract tools for Java, is that preconditions in subclasses are considered to be additions to any inherited preconditions, and combined by disjunction. (Some tools require a slightly different syntax for assertions in subclasses in order to emphasize this point.) In this way, if a method inherits a precondition α and adds another precondition β, the actual precondition in the subclass is taken to be α ∨ β, which, by construction, is weaker than the inherited precondition. This means that preconditions never have to be copied, and the correct relationship is established automatically and does not need to be checked at runtime. This approach is therefore more succinct as well as more efficient, and is the one taken by Jose. (However, Jose can easily be modified to support the first approach as well.) The treatment of postconditions and invariants is similar, except that these may only be strengthened by subclasses, and are therefore combined by conjunction rather than disjunction. 1 The pronunciation of the Spanish name Jos´ e is very similar to that of the Hebrew word for “contract.”

2.2 Old Values in Postconditions In order to allow postconditions to refer to expressions evaluated on entry to the method, these values need to be computed and kept somewhere until the end of the method computation. Variables declared for holding these values need to have an appropriate type. The tool should therefore compute the type of the expression in order to declare the variable correctly. Another question is where these values should be kept; this is further complicated by the need to keep values in $prev expressions from postconditions declared for the same method at various levels of the inheritance hierarchy. Another complicating factor is that $prev expressions may turn out not to be evaluated; for example, they may be qualified by a condition that happened to be false in some execution. It is quite possible that the evaluation of the expression inside $prev results in an exception in such cases. For example, suppose we want to specify that a certain method changes neither the number of elements of the stack, nor the top element of the stack, if there is one. We would write two postconditions: count() == $prev(count()), and count() == 0 || top() == $prev(top()). (With tools that support an implication operator, such as ==>, the second postcondition would more perspicuously be written as count() != 0 ==> top() == $prev(top()).) However, as far as the tool is aware, the call to top() in this postcondition needs to be evaluated when the method computation begins, in every case. At that point, an exception will be thrown when the count is zero. This exception does not indicate any error, because in fact the value of the $prev expression will not be required. The programmer can prevent such an exception by putting a conditional inside the $prev expression; in the example above, by changing the second postcondition to count() == 0 || top() == $prev(count() == 0 ? null : top())

Alternatively, the tool itself could handle this problem by catching the exception, and only throwing it during the computation of the postcondition if the value of the $prev expression is actually needed. However, the overhead of a try/catch block around every $prev expression may not be acceptable. If so, the $prev keyword could be kept for normal uses, and a different keyword (e.g., $safe_prev) could be used for the cases where exceptions need to be caught.

2.3 Constructors The precondition of a constructor needs to be checked before any computation in the constructor begins; this

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

means that it should occur even before the call to the super constructor. Constructors are not inherited, and therefore the preconditions of a constructor in a superclass do not apply to constructors of its subclasses. However, when the subclass constructor calls its super constructor, this call needs to satisfy the preconditions of the particular super constructor being called. This check also needs to occur before the super call. Instrumenting these checks is quite difficult, because Java does not allow any code to be inserted before super constructor calls. The situation for invariants is different. Invariants of all superclasses must be satisfied when the new object is ready. This time point is at the end of the lowest-level constructor (the first one called). It is wrong to check invariants when super constructors finish execution, since the object is not yet fully initialized. This applies even to inherited invariants. For example, an abstract Stack class might define the invariant capacity() >= 0. In this class, capacity() is a getter method for an internal field. A class ArrayedStack could extend Stack and keep its elements in an array called rep. This class will then redefine capacity() to return rep.length. The constructor for ArrayedStack creates this array, but it is still null when the super constructor (from Stack) finishes. If the invariant of Stack is evaluated at this point, a NullPointerException will be thrown. Therefore, it is necessary to evaluate all invariants, including inherited ones, only at the end of the lowest-level constructor. This condition is not easy to detect. For example, JML [4], a source-to-source translator, defines in each class a private field that is initialized to false, and set to true at the end of each constructor of the class. A protected method returns the value of this variable. Invariants are checked at the end of the constructor only when the method returns true. Because the method is overridden in each subclass to return the value of its own private variable, the method will return true only at the end of the lowest-level constructor. This is considerable overhead. Constructor postconditions pose the greatest difficulty. For the reasons explained above, they cannot be evaluated at the end of the super constructors. For example, think of the postcondition capacity() == n on the constructor for Stack, where n is the contructor’s parameter. This postcondition cannot be evaluated at the end of the super constructor, for the same reason that an invariant involving capacity() cannot be evaluated at that time. But postconditions of the super contructor cannot be evaluated at any later point, since there is no requirement that they hold later. Therefore, only the postconditions on the lowest-level constructor should be evaluated at all. (This is consistent with the theory to the extent that this postcondition needs to be repeated for ArrayedStack anyway, as there is no in-

heritance relationship between constructors. While errors in the super constructor might go undetected, there is really no cure for this problem.)

2.4 Preventing Infinite Recursion Assertions may refer to other methods, including those of the same class. Any tool that instruments the program to check assertions needs to be careful not to enter into an infinite recursion during assertion checking. For example, if the Stack class has an invariant capacity() >= 0, and this invariant is checked upon entry to the capacity method, an infinite recursion will result. Eiffel takes a conservative view, and turns off all assertion checking while it checks any assertion. The rationale for this is that methods used in assertions should be verified separately, before being used to specify the behavior of other parts of the program. It is possible to check more assertions without getting into an infinite recursion; Jose tries to check as much as possible (see Section 5.5).

2.5 Incremental Compilation Because inheritance relationships between classes affect the assertions that need to be checked, design-by-contract tools need to know this information. If all the hierarchy and all contracts are given, it is relatively easy to collect all the information and hard-code it into the instrumented code. For example, all preconditions of a method can be collected into one big disjunction. However, this means that whenever a class changes, all its subclasses need to be re-instrumented, and full sources have to be available at that time. This could be a serious problem for a large system, especially if not all sources are available. Ideally, it should be possible to instrument each class independently of the others. For preconditions, for example, this implies that each class should somehow contain a means of computing its own preconditions, to be invoked from subclasses as necessary. In this scheme, in order to instrument a subclass it is only necessary to know which methods are inherited and whether the superclass or any implemented interfaces have contracts, but not what the exact contents of these contracts are. (This information can be discovered from the class files, or at runtime if we are willing to indulge in the overhead of exception handling or reflection.)

3 Instrumentation There are several ways to instrument Java programs. Perhaps the simplest is source-to-source transformation, where a pre-processor generates new Java files that are compiled using a standard Java compiler. This approach has the great

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

benefit that it can use any Java compiler and is not platformspecific. Another approach is to instrument the class files, either by producing new ones or during class loading. This requires more intimate knowledge of the Java Virtual Machine (JVM), but is still portable. A third approach is to modify the JVM itself in some way. This allows implementation freedom that may be unavailable in the other two approaches; for example, it could make it possible to execute arbitrary code before the super constructor, which is not allowed by the Java language or the JVM. However, this makes the tool dependent on a single JVM, and possibly only on a specific version of that JVM. Much of the technical part of aspect-oriented programming is about instrumentation of programs. We have therefore chosen to use AspectJ [9] for this task. AspectJ is an extension to Java that allows the programmer to specify aspects whose code is inserted into existing Java classes. It is portable and compatible with all JVMs (above version 1.1). Although the semantics of AspectJ has not been fully documented, and we have found some inconsistencies in its treatment of call and execution pointcuts [3], we have been able to implement all the features required for design by contract using AspectJ. An aspect consists of advice, which are pieces of code to be invoked when specific events occur during execution of the instrumented program. These events are called join points, and include method calls, reading and modifying fields, handling exceptions, and more. A pointcut is a specification for a set of join points; for example, the pointcut get(* C.x) contains all join points in which the value of variable x of class C is read. There are three types of advice: before advice executes before the join point, after advice executes after it, and around advice replaces it completely (but can optionally invoke the original code). We explain the salient features of AspectJ as we use them in the sequel. For a full treatment see, e.g., Laddad [9].

4 Related Work There are several design-by-contract tools for Java. These include iContract [8], JMSAssert [12], Jcontract [15], Jass [2], JML [4], conaj [11], Barter [16], and Contract4J [1]. Some of these have been evaluated for use by a course given by one of the authors [5], and two (iContract and JMSAssert) have actually been used in that course over several semesters each. Some of these tools are research prototypes, while others are mature systems used by many programmers. It is important to note that many of the more mature tools extend the design-by-contract concept in various ways. For example, JML and Jass support quantifiers in assertions as well as loop variants and invariants, and JMSAssert has a powerful scripting language that can be used in asser-

tions. JML is also used for program verification, and Jass has a unique feature called “trace assertions,” which are assertions about the dynamic behavior of objects over time. However, the rest of this discussion concentrates on the use of these tools for contract checking. Most of these tools are source-to-source transformers; notable exceptions are JMSAssert, which uses a Windows DLL that only works with the classic 1.3 JVM, and conaj, Barter, and Contract4J, which employ AspectJ. Each of the tools we evaluated had subtle problems with the way asssertions are checked. For example, some evaluate class invariants at the end of super constructors, others do not check preconditions for super constructors, or have trouble with the types of new variables they generate. Some do not implement the behavioral subtyping principle at all, or get it wrong (typically combining preconditions by conjunction instead of disjunction). Some tools bypass the whole problem of keeping old values by simply keeping a clone of the current object at the beginning of the method call and providing the clone for use in postconditions. This approach suffers from several problems. First, it does not work at all when the object is not cloneable. Second, it is not expressive enough. The expression whose old value we want may not be copied by the clone operation; it could even be a static field of the class, or derived from some other object. Third, it could waste a lot of resources if the object contains a lot of state, even when only a small part of that state is required for the postcondition. Like Eiffel, most tools do not check assertions recursively. This is done in different ways, not always successfully. For example, Jass only supports this to one level. It copies the body of each method to an internal method that is not instrumented; calls inside assertions will be made to this internal method. However, assertions for calls to methods of other classes, as well as calls from inside these special methods, will be checked, and infinite recursion may still result. As mentioned in Section 2.1, most tools inherit assertions from superclasses and combine them with subclass assertions in the appropriate way. Jass and conaj, however, check the relationships between assertions instead. It seems to us that many of the problems with these tools are a result of instrumentation difficulties. We have therefore decided to rely on AspectJ for the instrumentation of the program, and to concentrate on the generation of the correct aspects from the given contracts. This is discussed in the next section.

5 From Contracts to Aspects This section describes the way in which Jose translates the contract into aspects. This discussion ignores many

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

issues that are important for a general-purpose tool, such as the prevention of name conflicts, comprehensible errorreporting, conciseness, etc. For brevity of the presentation we treat each issue separately, and use short names and anonymous pointcuts, even though the Jose tool produces somewhat different code.

5.1 Preconditions Suppose a method with signature void m() in class C has a precondition α. The simplest AspectJ code to check the precondition would be: before() : call(void C.m()) { if (!α) throw new PreconditionViolationException(); }

This code snippet, part of an aspect, declares advice that is invoked before every call to the method void m() of class C or any of its subclasses. The advice checks the precondition, and throws an exception if it is violated. This solution has a number of errors: (1) it does not capture all calls; (2) the precondition is evaluated in the wrong context; and (3) it ignores any inherited contract. We deal with each of these in turn. AspectJ call pointcuts are instrumented at the client (caller) code. While it is natural to instrument clients using call pointcuts, this fails to capture all client calls. For example, any call made using reflection will not be caught. Also, the current AspectJ compiler needs to have access to the client bytecode in order to instrument it; if this is not available, no checks will be performed. Even more important, matching of call pointcuts depends on the static type of the variable [3]. However, the semantics of the call depend on the dynamic type of the object. For these reasons, Jose uses execution pointcuts, which instrument the supplier code rather than the client’s. Both call and execution pointcuts apply to all subclasses of C [3]. This is unacceptable in this case, since it means that for any subclass of C, if the precondition of C is not satisfied, an exception will be thrown from the advice defined for C above. However, the actual precondition of the method m in the subclass may be weaker. We therefore have to limit the advice only to direct instances of C. This is easily done by using the pointcut execution(void C.m()) && within(C). The two parts of this pointcut are combined using set intersection; the second set consists of all join points whose code is lexically contained in the class C (but not in any of its subclasses). If C has an inner classes, the conjunct !within(C.D) needs to be added for each inner class D. The second problem with the above code is that the precondition α is defined in the context of the method m of

class C. However, as written above, α will be evaluated in the context of the aspect rather than the class C. Thus, unqualified references to methods and fields will be interpreted incorrectly. It is possible to solve this problem by analyzing the expression and qualifying references appropriately. For example, any unqualified call to a method f() would be replaced by current.f(), where current is a variable denoting the target of the call. It is captured by the pointcut this(current), which binds the variable current to the current object. However, a simpler solution is to use inter-type method declaration, which inserts a new method into class C:2 public boolean C.check_precondition_m() { return α; }

The C. prefix tells AspectJ to insert the method into the class C. The advice now becomes before(C current) : execution(void C.m()) && within(C) && this(current) { if (!current.check_precondition_m()) throw new PreconditionViolationException(); }

The third problem is that a violation of the precondition at the current level is not an error if a precondition is satisfied at another level. This follows from the fact that effective preconditions of a method is the disjunction of all preconditions from this and higher levels (see Section 2.1). A straightforward solution would be to statically collect the expression for the effective precondition during compilation, and insert it into the new method. However, this violates the incremental compilation requirement (Section 2.5). This is easily fixed by having each level call the corresponding method in its superclass: public boolean C.check_precondition_m() { return α || super.check_precondition_m(); }

Of course, we also need to take care of preconditions defined in any implemented interfaces. Fortunately, AspectJ supports method introduction into interfaces as well. Into every interface I that defines the method m we insert a method check_precondition_I_m that checks its precondition, also calling the corresponding methods for any interfaces that I itself implements. So if C implements the interfaces I and J, its precondition-checking method will be: 2 If the method has arguments, the name of the new method includes their types, in order to distinguish between overloaded methods.

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

public boolean C.check_precondition_m() { return α || super.check_precondition_m() || check_precondition_I_m() || check_precondition_J_m(); }

Note that the order of evaluation here is important. Preconditions from subclasses need to be checked before preconditions from their superclasses; furthermore, evaluation should be stopped as soon as a precondition for any level returns true. To see why this is so, think of a method that has a string parameter x and two preconditions: x != null and !x.equals(""). A subclass might weaken this precondition by adding another precondition, x == null, which means that a null value for x is also acceptable in the overriden implementation of this method. Suppose now that a client of the subclass correctly calls it with a null value. If preconditions are evaluated in the superclass first, a spurious exception may be thrown even for legal inputs.

5.2 Postconditions and Old Values Unlike preconditions, postconditions are combined by conjunction: if a postcondition at any level of the inheritance hierarchy is violated, the supplier is in error. Therefore there is no need to collect preconditions from all levels before deciding whether to throw an exception or not, as was done for preconditions. The complex feature here is the treatment of old values (Section 2.2). The straightforward solution is to use around advice that keeps old values in local variables of the advice itself. Suppose the method m has a postcondition γ($prev(exp)) in class C, where exp has type T . We insert a method into C to compute the value of the postcondition (note that in this case the method name contains the class, because we do not want postconditioncomputation methods in subclasses to override the corresponding methods in their superclass): public boolean C.check_postcondition_C_m(T prev1) { return γ(prev1); }

In addition, we need a method that computes the expression in the context of the class C: public T C.get_C_m_prev1() { return exp; }

The advice that activates this is: void around() : execution(void C.m()) && this(current)

{ T prev1 = current.get_C_m_prev1(); proceed(); if (!current.check_postcondition_C_m(prev1)) throw new PostconditionViolationException(); }

(Around advice replaces the original method body; the proceed pseudo-method invokes the original method of the join point from within the advice.)

5.3 Invariants Class invariants, like postconditions, are combined using conjunction, but cannot refer to old values. Their instrumentation would therefore seem to be straightforward: each class invariant would be instrumented separately, using before and after advice instead of the around advice needed for postconditions. However, because of the special requirements in instrumenting invariants for constructors (see Sections 2.3 and 5.4), we need a method that checks all invariants, including inherited ones. The scheme is therefore more similar to that used for preconditions (Section 5.1). For each class C whose invariant assertion is δ, and which implements interfaces I and J, Jose inserts the following method into C: public boolean C.check_invariant() { return δ && super.check_invariant() && check_invariant_I() && check_invariant_J(); }

An interface I with invariant θ, and which extends another interface J, will have a similar inter-type method: public boolean I.check_invariant_I() { return θ && check_invariant_J(); }

Invariants are checked at the end of the lowest-level constructor, and at the beginning and end of every non-private non-static method. For methods, instead of using around advice, which is more expensive, this invariant is invoked from before and after advice: before(C current) : execution(!private !static * C.*(..)) && within(C) && this(current) { if (!current.check_invariant()) throw new InvariantViolationException(); }

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

after(C current) : execution(!private !static * C.*(..)) && within(C) && this(current) { if (!current.check_invariant()) throw new InvariantViolationException(); }

5.4 Constructors As shown in Section 2.3, constructor preconditions need to be checked for each constructor call, including super constructors. These checks need to be performed before calling any super constructor, since any information that the precondition refers to (such as static fields or previouslycreated objects) could be changed during the super call. Postconditions should only be checked for the lowest-level constructor, and there is no inheritance of constructor postconditions. Invariants should be checked only at the end of the lowest-level constructor, but this check should include inherited invariants. Suppose we are given the following class definition:3 /** @invariant δ */ public class C extends B { /** @pre φ * @post ψ($prev(exp)) */ public C() { super("foo"); // ... } }

Preconditions should be checked for every constructor, without inheritance, and before the super constructor. Execution join points happen after the call to the super constructor, so we need to use a preinitialization pointcut instead of execution. (Preinitialization join points cover the code executed between the start of the constructor execution and the super call; this code includes the computation of the parameters to the super constructor.) public boolean C.check_precondition_C_new() { return φ; } before(C current) : preinitialization(C.new()) && 3 Assertions in Jose, as in several similar tools, are specified using the Javadoc tags @invariant, @pre, and @post.

this(current) { if (!current.check_precondition_C_new()) throw new PreconditionViolationException(); }

For the correct treatment of postconditions and invariants, we need to identify the lowest-level constructor. This is automatic with call pointcuts, which do not capture super contructors. However, as explained in Section 5.1, we need to use execution pointcuts, which do. This requires some circumlocution. The within construct does not help here, because every constructor is within its own class anyway. The way to tell whether a constructor for class C is not being called as a super constructor is to check that the actual class of the object is C. We need to resort to runtime tests, using an if pointcut, which can perform any test on any join point: after(C current) : execution(C.new()) && this(current) && if (current.getClass() == C.class) { if (!current.check_invariant()) throw new InvariantViolationException(); }

where the invariant-checking function is the one shown in Section 5.3. The treatment of postconditions is similar, except that any old value expression may not refer to the current object, which does not yet exist when the constructor starts. The methods for computing old values are therefore static: public static T C.get_C_new_prev1() { return exp; } public boolean C.check_postcondition_C_new(T prev1) { return ψ(prev1); } void around(C current) : execution(C.new()) && this(current) && if (current.getClass() == C.class) { T prev1 = C.get_C_new_prev1(); proceed(); if (!current.check_postcondition_C_new(prev1)) throw new PostconditionViolationException(); }

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

There is a flaw in this scheme, which is a consequence of the fact that constructor execution (and initialization) join points do not include the call to the super constructor. The old value is therefore computed after the super constructor, which might have changed its value. In principle, this value should be computed before any super constructor. The difficulty is where this value should be stored until it is needed by the postcondition. It cannot be stored in the object, since it does not exist before the constructor call. It cannot be stored in the advice, since the advice is not activated soon enough. Storing it in the aspect is complicated by multiple threads calling the same (unsynchronized) constructor, and by the (admittedly rare) case of a constructor that creates another object of the same class. It is possibe to keep in the aspect a (properly synchronized) mapping from threads to stacks of old values. This is substantial overhead for a relatively rare issue, and is not implemented in Jose.

5.5 Recursive Assertion Checking As mentioned in Section 2.4, Eiffel only allows one level of assertion checking. This policy is easy to enforce in Jose, since all assertion checks are performed through advice. It is enough to conjoin the clause !cflowbelow(adviceexecution())

to all pointcuts used in advice that checks assertions. This will eliminate all join points that arise from the execution of any advice. We want to be more liberal, and allow recursive checking of assertions, without, of course, getting into an infinite recursion. in order to do that, we need to analyze the possible types of recursion in assertion checking. First, there is recursion between invariant checks. Whenever an invariant calls a method of the same class, invariants will have to be checked for that method call, immediately leading to infinite recursion. In any case, there is no point in checking invariants for methods called during invariant checking, since the point of the invariants is to make sure that the object is in a consistent state. Since assertions should never have any side effects, there is no need for this recursion at all. We therefore add the clause !cflowbelow(boolean C.check_invariant()) to the advice responsible for checking invariants. The example from Section 5.3, instrumenting invariant checks on method entry, now becomes: before(C current) : execution(!private !static * C.*(..)) && within(C) && !cflowbelow(execution (boolean C.check_invariant())) && this(current) { if (!current.check_invariant())

throw new InvariantViolationException(); }

and the other cases (invariant checks on method and constructor exits) are similar. Precondition recursion can happen when the precondition of some method m uses a different method r, which either calls m or has a precondition or postcondition involving m. This situation is quite rare, but not difficult to treat. All we need to do is add another clause to prevent this recursion; the example from Section 5.1 now becomes: before(C current) : execution(void C.m()) && within(C) && !cflowbelow(execution (boolean C.check_precondition_m())) && this(current) { if (!current.check_precondition_m()) throw new PreconditionViolationException(); }

Similarly, the advice for postconditions (Section 5.2) is changed to: void around() : execution(void C.m()) && !cflowbelow(execution (boolean C.check_postcondition_C_m(T ))) && !cflowbelow(execution(T C.get_C_m_prev1())) && this(current) { T prev1 = current.get_C_m_prev1(); proceed(); if (!current.check_postcondition_C_m(prev1)) throw new PostconditionViolationException(); }

Note that this is still a little too restrictive: it prevents calls to the same assertion-checking method even for different objects. For example, the invariant of a class that represents elements of a linked list might contain the assertion next() == null || count() == next().count() + 1

This assertion refers to a method of another element of the same class, for which invariants will not be checked according to the scheme above. If there are multiple simultaneous join points that match the same control-flow pointcut, AspectJ provides access only to the current object of the innermost join point, which makes it difficult to capture this case. In order to do that, we would have to keep track of objects involved in the control flow using special-purpose code. This overhead does not seem justified in this case.

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

6 Discussion Implementing design by contract using aspects is nontrivial, and places high requirements on the aspect-oriented technology used. Because Jose generates its own aspects, we had to have a precise semantic definition for the tool we used, AspectJ. Such a specification does not yet exist, and we found some internal inconsistencies in the current implementation of AspectJ [3]. Beyond its basic functionality, certain features of AspectJ made the implementation of Jose easy, while others had to be worked around. The lessons we learned about AspectJ are described next.

6.1 Lessons Learned about AspectJ On the whole, we found AspectJ to be appropriate for our purposes. Jose is a relatively small application (it currently consists of 15 classes, excluding parsing and errorchecking), completely focused on the translation of contracts into aspects. Besides the obvious capabilities of instrumenting arbitrary methods, the following features of AspectJ were particularly useful: • Especially important was the capability of inserting code before the super constructor, using preinitialization join points. This allowed us to solve some of the thorny problems that plague other tools, especially (but not only) source-to-source transformers. • Another useful feature of AspectJ is inter-type method introduction. This made the evaluation of assertions in the right context very easy, although with some parsing effort the assertions could be re-written for inclusion inside the aspect rather than the class being instrumented. A rather surprising capability of AspectJ is the introduction of methods into interfaces. This helped our goal of compilation independence, because the assertion-checking code could be inserted into the interface by the aspect generated from that interface. Without this capability, this code would have had to be put in the aspect itself, making it more cumbersome to access. • A crucial feature is the ability to write privileged aspects, which can access all members of the target class, even private ones. Postconditions and class invariants (but not preconditions) are allowed to access private members. Such assertions are not meaningful to clients of the class, but are important for the developers. In particular, the implementation invariant [14] specifies the state of corret objects, and often refers to private fields. In Eiffel, such assertions are an integral part of the class to which they refer, and naturally have full access. When using aspects, the assertions appear inside the aspect, yet still need to have full

access. Priviledged aspects are therefore necessary to support this functionality. • The ability to use arbitrary conditions in pointcuts was most useful in those cases where the other AspectJ constructs could not define the precise conditions needed. Without it, for example, there would be no way to identify the lowest-level constructor using execution pointcuts (Section 5.4). Several features of AspectJ made the job of writing Jose more difficult. For most, but not all, we found workarounds, as described above. • Perhaps the most problematic issue was the correct treatment of constructors (Section 5.4). While call pointcuts capture only the lowest-level constructor, execution pointcuts capture all constructor calls, including super constructors. While there may be implementation concerns that make this the easy choice, it is hard to justify from the user’s point of view (that is, based on theoretical principles of aspect-oriented programming). It seems reasonable that either both types of pointcuts or none should capture calls to super constructors; what’s more, there should be an easy way of specifying whether those are intended or not. • Another difficult issue with constructors is that constructor execution join points do not include the whole body of the constructor. Specifically, the code they cover starts after the call to the super constructor. This makes it very difficult to write around advice for constructors. In fact, as mentioned above, we decided not to add to Jose the considerable overhead of doing this right. In this case, too, it is very likely that implementation considerations defined this behavior; and, again, it is hard to justify theoretically. Since AspectJ can, in fact, insert arbitrary code before the super constructor, as evidenced by preinitialization join points, we believe that constructor execution join points should include the whole constructor body. • AspectJ provides convenient means of capturing all the relevant information about call and execution pointcuts: the current object and target, and the arguments. Only limited information is exposed for control-flow pointcuts (cflow and cflowbelow). Sometimes, as shown in Section 5.5, this information would be useful, and is hard to get without support from AspectJ. • Eiffel (and some of the Java tools, such as JML [4] and Jass [2]) support the instrumentation of loop variants and invariants. A loop variant is an integer-valued expression that must be non-negative throughout the loop, and must decrease by at least one in every pass.

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006

The existence of a loop variant proves that the loop always terminates. Loop invariants are conditions that must be true whenever control passes through the begninning of the loop, in every pass. These are used to prove the correctness of the loop. Because AspectJ does not provide loop join points, it is impossible to instrument loop variants and invariants in any tool based on AspectJ. From the point of view of a design-by-contract tool, this is unfortunate. Loop variants and invariants are a natural extension of the design-by-contract methodology, but a tool like Jose, which relies on AspectJ to handle the tricky parts of instrumenting contracts, will not be able to support them. LoopsAJ [7] is an extension of AspectJ that can capture common types of loops. Such extensions are inherently limited by the fact that loops in Java are not named, nor can labels or annotations be used to uniquely identify loops. Furthermore, LoopsAJ can identify the join point before the loop, but does not provide a join point at the beginning of the loop body, which is required for instrumenting loop assertions.

6.2 Other Issues A major usability problem with generative tools is that the user may get compilation error messages about automatically-generated code, even though the source of the error is in assertions written by the user. In an early implementation of Jose, syntax errors in assertion would cause error messages that refer to the aspects generated by Jose. We have therefore added a parser to Jose; the parser’s main responsibility is to issue error messages while generating the aspects; these messages refer to the original assertions in the user’s source files. Finally, the introduction of generics in Java 5 makes it necessary to support assertions with generic types. The recently-released AspectJ 5 supports generics as well, and this capability should therefore be easy to integrate into Jose as well. This work is now in progress.

6.3 Conclusion We have presented Jose, a design-by-contract tool for Java that uses AspectJ for instrumenting the code. A unique contribution of this approach is that it can be generalized to other object-oriented languages for which aspect-oriented models exist. The same principles of translating contracts to aspects should hold for other languages as well, although certain details might have to change based on the particular characteristics of the target language and those of its aspectoriented extension. Jose has already been used in our Object-Oriented Software Construction course [5] in 2005, and we are now

working on streamlining this tool in order to make it useful to the community in general. Our eventual aim is to publish Jose as an open-source tool.

Acknowledgments We thank Oded Nahir, Rami Sass, and Vladi Polonsky for their help in implementing Jose, and Amiram Yehudai and Eric Bodden for helpful comments on earlier drafts of this paper.

References [1] Aspect Research Associates. Contract4J: Design by contract for Java. http://www.contract4j.org. [2] D. Bartetzko, C. Fischer, M. M¨oller, and H. Wehrheim. Jass—Java with assertions. Electronic Notes in Theoretical Computer Science, 55(2), 2001. [3] O. Barzilay, Y. A. Feldman, S. Tyszberowicz, and A. Yehudai. Call and execution semantics in AspectJ. In Proc. Foundations of Aspect-Oriented Languages (FOAL), Mar. 2004. [4] L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. In T. Arts and W. Fokkink, editors, Eighth Int’l Workshop on Formal Methods for Industrial Critical Systems (FMICS ’03), pages 73–89, June 2003. [5] Y. A. Feldman. Teaching quality object-oriented programming. ACM J. Educational Resources in Computing, 5(1):1– 16, 2005. [6] R. B. Findler and M. Felleisen. Contract soundness for object-oriented languages. In Proc. 16th ACM Conf. Object Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 1–15, 2001. [7] B. Harbulot and J. R. Gurd. A join point for loops in AspectJ. In Proc. 5th Int’l Conf. Aspect-Oriented Software Development (AOSD), Mar. 2006. [8] R. Kramer. iContract—the Java design by contract tool. In Proc. Technology of Object-Oriented Languages and Systems, TOOLS-USA. IEEE Press, 1998. [9] R. Laddad. AspectJ in Action: Practical Aspect-Oriented Programming. Manning, 2003. [10] B. H. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Trans. Programming Languages and Systems, 16(6):1811–1841, 1994. [11] D. H. Lorenz and T. Skotiniotis. Contracts as aspects. Technical Report NU-CCIS-03-13, College of Computer and Information Science, Northeastern University, 2004. [12] Man Machine Systems. Design by contract tool for Java—JMSAssert, 2002. http://www.mmsindia. com/JMSAssert.html. [13] B. Meyer. Eiffel: The Language. Prentice Hall, 1990. [14] B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd edition, 1997. [15] Parasoft Corp. Jcontract home page, 2002–2004. http://www.parasoft.com/jsp/products/ home.jsp?product=Jcontract. [16] V. Szathmary. Barter — beyond design by contract. http: //barter.sourceforge.net.

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06) 0-7695-2678-0/06 $20.00 © 2006