My favorites ▼ | Sign in
Project Home Downloads Wiki Issues Source
Summary   People
Project Information
Members

Note: Development on Java on Contracts has been suspended for now, as I'm currently working on a successor for C4J.

There are so many DBC libraries for Java out there, yet none of them that I've looked at met the following criteria:

  • easy to use with little overhead (i.e. no extra class-hierarchies for contracts)
  • complete code-integration (no comment-parsing stuff that needs adjustment as soon as you change a method- or parameter-name) in pure Java
  • being able to not only throw an assertion when a contract fails, but also to silently log the contract violation and leave the application running (e.g. in production systems)
  • easily extensible with own contracts or checks
  • assign contracts to foreign classes (e.g. preventing to call "new Integer")
  • lots of more ideas, e.g. profiling or logging method calls, customizable behavior for each contract definition, etc.

See Installation for instructions on how to use JOC.

Features

Implemented in Version 0.3

Pre-Conditions bound to Method Parameters

The pre-condition will be checked before the method is executed. Subclasses need to explicitly define the pre-condition again, as they are allowed to accept a wider range of values. 

@JOCEnabled
public class CashTerminal {
  public void withdraw(@GreaterThanLong(0) long amount) {
    // withdraw money from customer's bank account
  }
}

Invariants bound to Fields

The invariants will be checked before and after a method of the class or subclasses is executed. For constructors, it will only be checked after a constructor of this class has been executed. This is sufficient, as subclasses are required to call a constructor of their superclass anyway. 

@JOCEnabled
public class Account {
  @NotNull
  private Customer customer;
}

Post-Conditions

For simple post-conditions, the contract annotations check the behavior of the return value of the method. 

@JOCEnabled
public class Customer {
  @ContainsString("Welcome")
  public String getWelcomeMessage() {
    // generate Welcome Message for Customer
  }
}

Writing own Contracts

Own contracts can be written very easily. For example, this is the complete implementation of the @GreaterThanLong contract. 

@Documented
@Target({ ElementType.FIELD, ElementType.PARAMETER, ElementType.METHOD })
public @interface GreaterThanLong {
  long value();
}

public class GreaterThanLongContract extends Contract<GreaterThanLong> {
  @ForFieldEvaluateAtBeginningOfAllMethods
  @ForFieldEvaluateAtEndOfAllBehaviors
  @ForParameterEvaluateAtBeginningOfBehavior
  @ForMethodEvaluateAtEndOfMethodAndInherit
  public PartialEvaluationResult checkContract(GreaterThanLong annotation, long value) {
    return getResult(value > annotation.value(), "Value " + value + " is not greater than " + annotation.value() + ".");
  }
}

Of course, you're also encouraged to write a respective Unit Test and System Test.

Custom contracts need to be added to the configuration in order for JOC to be able to detect them. 

contract_joc.example.CustomContract = On

Pure methods

Methods being annotated with @Pure must not have any side effects, which means that neither the object's state itself nor any other object's state is being modified. This is implemented as follows:

  • No write-access to any fields (instance and static) on any class.
  • If methods from classes being annotated with @JOCEnabled are called, they must also be @Pure.

Also, custom contract methods are implicitly @Pure to ensure that using contracts won't have any side effects, with the exception of write access to their own fields.

Custom Post-Conditions

As post-conditions often heavily depend on the method they're used in, you might have to write your own post-conditions. A nice and refactoring-safe way of doing so without specifying new contracts is to give each post-condition its own class. 

@JOCEnabled
public class CashTerminal {
  protected Account account;

  @PostCondition(PostWithdraw.class)
  public boolean withdraw(int amount) {
    // withdrawing amount from the account, returns true on success
  }

  protected static class PostWithdraw {
    private int initialBalance;
    @BeforeCondition // optional and only needed if the post-condition needs values from the beginning of the method call
    protected void before(CashTerminal target, int amount) {
      initialBalance = target.account.getBalance();
    }
    @Condition // needs to return false on contract violation
    protected boolean after(CashTerminal target, boolean returnValue, int amount) {
      if (returnValue) {
        return initialBalance == (target.account.getBalance() + amount);
      }
      return initialBalance == target.account.getBalance();
    }
  }
}

The methods annotated with @BeforeCondition and @Condition get the object and the parameters of the method at the beginning and the end of the method execution respectively. To reduce code overhead and to ease refactoring, you can ignore parameters at the end of the parameter list, so in the example above, the parameter amount in method before could've been left out. @Condition also gets the return value as the second parameter, if the annotated method is returning a value.

Note that you should declare all fields, inner classes being used as post-conditions and their methods as protected, as potential subclasses overriding the method are implicitly using the same post-conditions.

Although target could be replaced with CashTerminal.this and the method parameter could be removed completely, using the method parameter is being enforced to keep the same pattern when moving post-conditions to external classes and thus to ease refactoring, as shown below.

Custom Post-Conditions as external classes

Of course, you don't have to use an inner class for post-condition-classes and can use a normal class just as well. This is especially useful if you need the same post condition in different classes. Access to class members should then be defined with interfaces, as is shown in the following example. 

public interface Withdrawable {
  public Account getAccount();
  public void withdraw(int amount);
}

@JOCEnabled
public class CashTerminal implements Withdrawable {
  private Account account;

  public Account getAccount() {
    return account;
  }

  @PostCondition(PostWithdraw.class)
  public boolean withdraw(int amount) {
    // withdrawing amount from the account, returns true on success
  }
}

public class PostWithdraw {
  private int initialBalance;
  @BeforeCondition
  public void before(Withdrawable target) {
    initialBalance = target.getAccount().getBalance();
  }
  @Condition
  protected boolean after(CashTerminal target, boolean returnValue, int amount) {
    if (returnValue) {
      return initialBalance == (target.account.getBalance() + amount);
    }
    return initialBalance == target.account.getBalance();
  }
  // there can also be multiple methods being annotated with @BeforeCondition and @Condition if there is more than one condition to be met
}

You could even move the @PostCondition annotation to the interface, if all implementing classes have to obey the PostWithdraw post-condition.

Custom Pre-Conditions and Invariants

If you need more specific pre-conditions and invariants than the ones provided by pre-conditions bound to method parameters and invariants bound to fields, you can arbitrarily define those just as you can define custom post-conditions. All features shown above are also available with these. 

@JOCEnabled
@Invariant(CashTerminal.BalanceGreaterEqualZero.class)
public class CashTerminal {
  protected Account account;

  @PreCondition(PreWithdraw.class)
  public void withdraw(int amount) {
    // withdrawing amount from the account
  }

  protected static class PreWithdraw {
    @Condition
    protected boolean before(CashTerminal target, int amount) {
      return amount > target.account.getBalance();
    }
  }
  protected static class BalanceGreaterEqualZero {
    protected boolean check(CashTerminal target) {
      return target.account.getBalance() >= 0;
    }
  }
}

Conditions retaining state with Hooks

Sometimes it is necessary to retain a state in between method calls, for example if you want to ensure that method A is called before method B. Hooks allow you to do just that. 

@JOCEnabled
public class CashTerminal {
  protected Account account;

  @PreConditionHook(LoginBeforeWithdraw.class)
  public void loginAccount(Account account) {
    // logging in the given account
  }
  @PreCondition(LoginBeforeWithdraw.class)
  public void withdraw(int amount) {
    // withdrawing amount from the account, needs the account
  }

  protected static class LoginBeforeWithdraw {
    private boolean isLoginAccountCalled = false;
    @AfterHook // being executed after the method annotated with @PreConditionHook
    protected void afterLoginAccount(CashTerminal target) {
      isLoginAccountCalled = true;
    }
    @Condition
    protected boolean condition(CashTerminal target) {
      return isLoginAccountCalled;
    }
  }
}

Profiling Contracts

If you have time-critical methods and want to track if a method execution exceeds a defined amount of time, you can use the @Profile contract. 

public class CashTerminal {
  @Profile(1000)
  public boolean authenticate(LoginCredentials credentials) {
    // calling the authentication service might take some time...
  }
}

The value provided defines the amount of milliseconds before a contract violation is thrown at the end of the method. You can also set the value to 0, which is only useful if you want to log the execution time for every method call using LogOn in the action configuration as explained below.

If you need greater precision, you can set the nano attribute of the @Profile annotation to true and the value will be interpreted in nanoseconds.

Enforce correctly overriding equals and hashCode

One of the most misunderstood contracts is the one of Object.equals. As such, it makes perfect sense to write an @Equals contract in order to enforce correctly overriding equals and hashCode. The @Equals contract implemented in JOC executes the following runtime-checks, whenever equals is being called:

  • equals(null) must return false
  • equal objects must return the same hashCode value
  • equals must be reflexive
  • equals must be symmetric

The only condition of Object.equals which is not implemented is transitiveness, as it would require at least 3 different objects, which would only be available when caching the runtime results.

Define contracts for foreign classes

So far, all contracts could only be directly assigned to your own classes. With JOC, you're also able to inject contracts into existing classes. For example, if you want to avoid using a problematic class in a library being used in your project, you can simply @Deny calling the constructors. 

@JOCExternalContract(ProblematicClass.class)
public class ProblematicClassContract {
  @Deny
  public ProblematicClassContract() { }
}

In order for JOC to find the external contract, you need to include it in the config. 

external_joc.example.ProblematicClassContract = On

Matching between the contract class and the class itself is done as follows:

  • fields are matched by name
  • constructors are matched by the types of the parameters
  • methods are matched by the method name and the types of the parameters

Note that post-condition and invariant contract inheritance is only done for subclasses who're also defining an external contract - even if it's empty.

General Configuration

Some general configuration parameters can be specified in joc.properties:

  • If all classes in a specific package and all of its subpackages should implicitly be annotated with @JOCEnabled, you can add the following command to the configuration: 

    • enable_package.name.to.be.enabled = On
  • All equals-methods can implicitly require the @Equals contract: 
    • _implicit-equals = On
  • All equals- or hashCode-methods are implicitly @Pure: 
    • _implicit-equals-pure = On
_implicit-hashcode-pure = On

Action Configuration

By default, once a contract is broken, JOC will throw an AssertionError and your application will most likely terminate. You can arbitrarily change this behavior for the whole codebase or specific packages, classes, methods, fields and specific contracts. The behavior can be configured using the following commands:

  • AssertOn - throw AssertionError (default)
  • AssertOff - don't throw AssertionError
  • LogOn - log contract violation
  • LogOff - don't log contract violation (default) 
# affects all contracts to be ignored, note that subsequent properties take precedence
action_* = AssertOff
# affects contracts in package joc.example and all its subpackages to silently log broken contracts
action_joc.example.* = LogOn
# affects all @NotNull contracts in package joc.example and all its subpackages to throw AssertionErrors without logging
action_joc.example.*@joc.contract.NotNull = AssertOn, LogOff

Implemented on trunk

Getters and Setters

Writing a conventional contract for a Setter can be a difficult task. At most, it includes the following:

  • The Setter must assign the field corresponding to its name, and only that field.
  • The Setter must have exactly one argument, and the type that argument must match the type of the field.
  • The Setter must actually set the value it is given in the argument to the field.

The @Setter contract takes care of all of the above and can be used for any method that must behave as a Setter.

The @Getter contract works in a similar fashion and makes sure, that the corresponding field's value is being returned. 

@JOCEnabled
public class Account {
  private int balance;

  @Getter
  public int getBalance() {
    return balance;
  }

  @Setter
  public void setBalance(int balance) {
    this.balance = balance;
  }
}

If you want to implicitly annotate all getters and setters with the @Getter and @Setter annotations, you can do so in the global configuration. 

_implicit-getter = On
_implicit-setter = On

Method Call Sequences

For some classes, it is important in which order the methods are being called. To enforce the call order on the class and all its subclasses, you can define a JOC call sequence by using the JOCCallSequence annotation. 

@JOCEnabled
@JOCCallSequence(CashTerminalCallSequenceProvider.class)
public class CashTerminal {
  public void loginAccount(Account account) { /* impl */ }
  public boolean authenticate(LoginCredentials credentials) { /* impl */ }
  public void withdraw() { /* impl */ }
  public void logout() { /* impl */ }

  protected static class CashTerminalCallSequenceProvider extends CallSequenceProvider<CashTerminal> {
    @Override
    public void callSequence(CashTerminal target) {
      call().loginAccount(null);
      before().withdraw();
      before().authenticate(null);
      before().logout();
    }
  }
}

The method callSequence in the CallSequence-class will be called by JOC when loading the class in order to make the proper code adjustments. Using the methods call and before, an arbitrary amount of call sequences can be defined. A call sequence starts by calling call and is followed by calling before for each following method in the call sequence.

The parameters for the methods being called in a call sequence are being disregarded. Thus, you can just use null for reference types and 0 or false for the respective primitive types.

Defining call sequences also works for interfaces and abstract classes, and all inherited classes must obey the defined call sequences in the class hierarchy.

Proposed

More General Configuration

  • Define a custom Throwable to be thrown on contract violations instead of AssertionError: 
    • _contract-violation-throwable = package.with.CustomThrowable

Scope Configuration

The scope configuration allows you to specify, in which context contracts will be evaluated. As seen in the example above, it makes no sense to @Deny calling all of the Integer constructors, as you could just as well @Deny the whole class itself. This is where the scope configuration comes in, allowing you to use certain contracts depending on the uppermost element of the call stack. The Integer example above could hence be completed with the following scope configuration, rejecting to use the @Deny contract for all invocations from java.lang. 

joc.scope.java.lang.Integer.*@Deny = Reject=java.lang.*

Auto-Profiling JOC

If you need to know how much JOC is slowing your code execution down, you can turn on auto-profiling in the configuration. JOC will then measure the time it takes to execute the production code versus the time it takes to bind contracts and evaluate them. This allows you to analyze which contracts you might want to turn off in production and where potential bottlenecks are.

The following configuration turns auto-profiling on and logs the complete results every 10 seconds. You can also specify a frequency of 0 seconds, in which case auto-profiling is still turned on, but you need to call joc.Profiling.logResults() to log the results at a specific point in time. You can also call joc.Profiling.getResults() to further analyze the results in your code. 

joc.profiling = 10000

Method Call Logging

Automated Specification Testing

One of the problems with DbC compared to TDD is that you don't have automated tests that can be run every time you integrate your changes into a central repository or even every time you hit Ctrl+S. The root of this problem is that you don't have any test data to begin with.

JOC allows you to provide test data that can be used to do automated specification testing. Basically, if a method is called and all pre-conditions and invariants are fulfilled in the beginning of a method call, the post-conditions and invariants must also be fulfilled at the end of a method call.

In order to provide JOC with the necessary test data, you can include a method in your test-class that is annotated with @JOCTest. In this method, you must provide instances of the class under test as well as instances of objects that can be used as method parameters. 

@JOCEnabled
public class CashTerminal {
  protected Account account;

  /* constructor, etc. */

  @PostCondition(/* a post-condition */)
  public boolean withdraw(@GreaterThanLong(0) int amount) {
    // withdrawing amount from the account, returns true on success
  }
  @PostCondition(/* another post-condition */)
  public void loginAccount(Account account) {
    // logging in the given account
  }
  @PostCondition(/* another post-condition */)
  public void loginAdminAccount(AdminAccount account) {
    // logging in the given account
  }
}

public class CashTerminalTest {
  @JOCTest
  public void jocTest(JOCTestEnvironment<CashTerminal> env) {
    CashTerminal terminal = new CashTerminal();
    /* initialize terminal for specification testing */
    env.addTarget(terminal);
    /* add more target objects */
    env.addParameter(new Account("bobby", "1234"));
    env.addParameter(new Account("alice", "5678"));
    env.onlyFor().loginAccount(null);
    env.addParameter(new AdminAccount("admin", "1337"));
  }
}
Powered by Google Project Hosting