DBC.PKGC

All package-private classes should have the '@invariant' contract

Description

This rule flags any package-private class without an '@invariant' contract: '$name'.

Example

 package DBC;
 
 class PKGC {
    /**
      * @pre size >= 0
      * @post ($return != null && $pre (size + 1) == size + 1)
      * @exception NegativeArraySizeException size < 0
      */
     public int[] allocate (int size) {
         return new int [size];
     }
     public String toString () {
         return "PKGC";
     }
     public static void main (String[] args) {
         new Strategy ().allocate (5);
     }
 }

Repair

Provide the `@invariant' Javadoc tag.

 /** @invariant toString ().equals ("PKGC") */