Home Directory / LeoDBC

Abstract

LeoDBC is a design-by-contract layer for the Java(tm) language.

The Design-by-contract methodology helps the developer and the designer to improve the correctness of the developed software by adding some information who say how the software is supposed to work.

This information take the form of method pre-condition, method post-condition, class invariant and assertions.

The method pre-condition are checked before any invokation is the method, the post-condition after the invocation of the method and the class invariants after any invokation of the method in the class.

This is a link to the Design-by-contract page on Wikipedia: link

LeoDBC peculiarities

There are several DBC frameworks for the Java language. The LeoDBC framework has some peculiarity:

• Is really simple to use for the software designer who should know only a part of the Java syntax.

• Is simple to use for the developer because the developing process don't change: you should only include a jar in your classpath and an argument when you want to launch the Java Virtual Machine. In short: it's really simple to integrate LeoDBC in a live develoment process.

• The contracts are exposed in the JavaDOC generated documentation so you can have better documentation for your project

• If you want to disable the contract checking you can launch the Java Virtual Machine in the standard way. If you want to remove the LeoDBC framework you can also remove the Jar File without corrupting your software.

• It can only be used with Java 1.5 or a more recent version because the conditions are expressed as annotations

Example

/**
 * Simple implementation of a generic vector using LeoDBC
 */
public interface SimpleVector<T> {
  /**
   * This method should add an element to the vector.
   * The "_store" variable in the pre/post condition is
   * a predefined LeoDBC variable who can be used to 
   * remember the "old" value of an expression.
   */
  @LeoPre("_store.putValue(\"oldlen\", length())")
  @LeoPost("_store.getInt(\"oldlen\")==(length()-1)")
  public void add(T toInsert);
  
  /**
   * Should return true if the method exist
   */
  public boolean search(T toSearch);
  
  /**
   * Should return the number of elements in the vector.
   * The $1 in the postcondition represent the return value of
   * the method.
   * The argument in the precondition are represented in a
   * positional number: $0 stands for the first argument, $1 for
   * the second and so on...
   */
  @LeoPost("$1>=0")
  public int length();
}

Documentation

The documentation for LeoDBC is included in the main distribution. It's only in italian... sorry!

Click here to directly download the pdf file.

Download

LeoDBC is released under a BSD-Like license and you can download it from here:

Latest update: 16/7/2007