DBC.PUBC

All "public" classes should have the '@invariant' contract

Description

This rule flags any "public" class that does not have an `@invariant' contract.

Example

 //From: "The Pragmatic Programmer", p.110.
 /**
   * @author 
   */
 
 public class PUBC {
     /**
       * @pre["item is not in list"] contains (item) == false
       * @post["item is in list"] contains (item) == true
       */
     public void insert (Item item) {
         // ...
     }
     public boolean contains (Item item) {
         //NYI:
         return false;
     }
 }
 
 class Item {
     Item (int value) {
         _value = value;
     }
     int getValue () {
         return _value;
     }
     void setNext (Item next) {
         _next = next;
     }
     Item getNext () {
         return _next;
     }
     private int _value;
     private Item _next;
 }
 

Repair

Provide the '@invariant' Javadoc tag.

 /**
   * @invariant["items are ordered"] {
   *    for (Enumeration e = elements; e.hasMoreElements (); ) {
   *        Item item = (Item) e.nextElement ();
   *        if (item.getNext () != null)
   *            $assert (item.getValue () < item.getNext ().getValue 
());
   *    }
   * }
   */