Home Directory / LeoDBC




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:


 * 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())")
  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...
  public int length();


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

Click here to directly download the pdf file.


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

tgz with sources and documentation Download
zip file with sources and documentation Download

Latest update: 16/7/2007