Alphonse Bendt |
Version vom: $Date: 2001/02/09 15:36:47 $
|
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.
TypEine 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 PreconditionsIn 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); Quantifierquantifier 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>:
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(); |
Zurück | Top | Hauptseite |