Home Directory / LeoDBC

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:

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:

16/11/2006
tgz with sources and documentation Download
zip file with sources and documentation Download

Latest update: 16/7/2007