DBC.PUBMPOST

All "public" methods should have the '@post' contract

Description

This rule flags any "public" class that does not have an `@post contract in its Javadoc.

Example

 package DBC;
 public class PUBMPOST {
     /**
       * @pre size () < MAX_SIZE - 1
       * @post peek () == object
       * @post size () == $pre (int, size ()) + 1
       * @concurrency sequential
       */
     public void push (Object object) {
         _storage [_top++] = object;
     }
     /** 
       * @pre size () > 0
       */
     public Object peek () {
         return _storage [_top - 1];
     }
     public int size () {
         return _top;
     }
 
     private Object _storage[] = new Object [MAX_SIZE];
     private int _top;
     private final static int MAX_SIZE = 100;
 }

Repair

Provide the `@post' contract.

     /**
       * @pre size () > 0
       * @post size () == $pre (int, size ())
       */