DBC.PPIC

All "private" classes should have the '@invariant' contract

Description

This rule flags any "private" class that does not have an `@invariant' contract.

Example

 package DBC;
 
 public class OrderedList {
     /**
       * @pre["item is not in list"] contains (item) == false
       * @post["item is in list"] contains (item) == true
       */
     public void insert (PRIC item) {
         // ...
     }
     public boolean contains (PRIC item) {
         //NYI:
         return false;
     }
 }
 
 private class PRIC {
     PRIC (int value) {
         _value = value;
     }
     int getValue () {
         return _value;
     }
     void setNext (PRIC next) {
         _next = next;
     }
     PRIC getNext () {
         return _next;
     }
     private int _value;
     private PRIC _next;
 }

Repair

Provide the `@invariant' contract.