DBC.PRIMPRE

All "private" methods should have the '@pre' contract

Description

This rule flags any "private" method that does not have an `@pre' contract in its Javadoc.

Example

 package DBC;
 public class PRIMPRE {
     /**
       * @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;
     }
     /** @post $return == (size () == 0) */
     private boolean isEmpty () {
         return _top == 0;
     }
 
     private Object _storage[] = new Object [MAX_SIZE];
     private int _top;
     private final static int MAX_SIZE = 100;
 }

Repair

Provide the `@pre' contract.