DBC.PKGMPOST

All package-private methods should have the '@post' contract

Description

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

Example

 /** @invariant toString ().equals ("Strategy") */
 class PKGMPOST {
    /**
      * @pre size >= 0
      * @exception NegativeArraySizeException size < 0
      */
     int[] allocate (int size) {
         return new int [size];
     }
 }

Repair

Provide the `@post' Javadoc tag.

 
 /**
   * @pre size >= 0
   * @post ($return != null && $pre (size +1) == size + 1)
   * @exception NegativeArraySizeException size < 0
   */