DBC.PRIMPOST

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

Description

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

Example

 package DBC;
 public class PRIMPOST {
     /**
       * @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 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 `@post' contract.

 /** @post $return == (size () == 0) */