DBC.PKGMPRE

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

Description

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

Example

 package DBC;
 
 /** @invariant toString ().equals ("Strategy") */
 class PKGMPRE {
    /**
      * @post ($return != null && $pre (size + 1) == size + 1)
      * @exception NegativeArraySizeException size < 0
      */
     int[] allocate (int size) {
         return new int [size];
     }
 }

Repair

Provide the `@pre' condition.

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