Alphonse Bendt
Version vom: $Date: 2001/02/09 15:36:47 $

javadoc mit iDoclet

Projektdokumentation | Projekthandbuch | Programmierrichtlinien | javadoc - Styleguide


Zurück Hauptseite
javadoc ist in JAVA geschrieben. Es ist möglich die Fähigkeiten von javadoc anzupassen um andere Zielformate als html zu unterstützen oder auch um andere Tags nutzen zu können.Genau dies tut iDoclet
Bei Benutzung von iDoclet kann man die Tags @pre, @post und @invariant benutzen um Vorbedingungen, Nachbedingungen und Invarianten im JAVA - Code festzuhalten
/**
 * Person.java
 *
 * @author <a href="mailto:writer@dot.com">Author</a>
 * @version $Id: JavaDoc.html,v 1.3 2001/02/09 15:36:47 hackenbe Exp $
 *
 * @invariant age_ > 0 // alter ist immer groesser 0
 */

public class Person {

  public int age_;

  /**
   * Beschreibung der Methode <code>getAge</code>
   * @post return > 0 // alter ist positiv
   */
  public int getAge() {}

  /**
   * Beschreibung der Methode <code>setAge</code>
   * @pre age > 0 // alter ist positiv
   */
  public void setAge(int age) {}
}
iDoclet kann dann aus der java - Datei eine html - Datei erzeugen und die Tags entsprechend umsetzen.

Es gibt einen Präprozessor der aus java Dateien mit solchen Tags Code erzeugen kann der Assertions enthält. Wird dann z.B. setAge(-1) aufgerufen, wird eine Exception ausgelöst.
Leider gibt es keine zusammenhängende Dokumentation. Man kann sich nur auf die Release Notes und ein Beispiel beziehen. Ich versuche hier folgend eine Zusammenfassung aus beiden Dokumenten anzugeben

Typ

Eine Condition hat einen booleschen Typ und kann von einem Kommentar gefolgt werden:
/**
 * @pre age > 0 // weiterer Kommentar
 */
public void setAge(int age);

/** 
 * @pre name != null // ...
 * @name.length() > 0 // ...
 */
public Room(String name);

Variable aus Preconditions

In Postconditions kann mit var@pre eine Variable aus den Preconditions referenziert werden.
/**
 * @pre !availableOfficePool.contains(employee.getOffice())
 *
 * @post availableOfficePool.contains(employee.getOffice()@pre)
 * @post employee.getOffice()@pre.isAvailable() // old office is vacant now (has no owner)
 */
public void move(IEmployee employee, IRoom newOffice);

Quantifier

quantifier evaluiert zu wahr wenn die domain leer ist oder mindestens ein element die bedingung erfüllt. allgemeine Form: forall/exists T t in <domain> | ...
wobei <domain>:
  • java.util.Enumeration
  • java.util.Iterator
  • ein Array aus primitiven Typen oder Objekten
    forall int v in arr | v > 12 // arr is an int[]
  • ein Bereich primitiver Typen
    forall int i in 0 .. arr.length-1 | i > 12 // arr is an int[]
    forall int i in arr.length-1 .. 0 by -1 | i > 12 // arr is an int[] counting down
    forall float f in 0.0 .. 10.0 by 0.1 | condition(f)
    
  • jeder Typ der eine der folgenden Methoden implementiert
    java.util.Enumeration elements();
    java.util.Iterator iterator();
    
    z.B. java.util.Vector oder jede java.util.Collection Klasse
    forall Person p in company.getEmployees() | ... // company.getEmployees() ist vom Typ List
    

implies

/** 
 * @invariant getRooms().isEmpty() implies getEmployees().isEmpty() // no rooms, no employees
 */

Conditions über mehrere Zeilen

/**
 * @invariant forall IEmployee e1 in getEmployees().elements() |
 *            forall IEmployee e2 in getEmployees().elements() |
 *            (e1 != e2) implies e1.getOffice() != e2.getOffice() // a single Office per employee
 */

mit return kann der Rückgabewert referenziert werden

/**
 * @post return == true implies exists IRoom r in getRooms().elements() | r.isAvailable()
 * @post return == false implies forall IRoom r in getRooms().elements() | !r.isAvailable()
 */
public boolean roomsAvailable();


Links


Zurück Top Hauptseite