    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.ast;
    004
    005    /** Various utility methods. */
    006
    007    public class Util {
    008
    009      /** Returns the size of the AST <code>n</code>.  The size
    010        * includes the size of all children nodes, even children
    011        * nodes that are <code>null</code>.
    012        **/
    013      //@ ensures 0 < \result;
    014      public static int size(/*@ non_null */ ASTNode n) {
    015        int t = 1;  // count this node
    016
    017        int k = n.childCount();
    018        for (int i = 0; i < k; i++) {
    019          Object c = n.childAt(i);
    020
    021          if (c instanceof ASTNode) {
    022            t += size((ASTNode)c);
    023          } else {
    024            t += 1;
    025          }
    026        }
    027
    028        return t;
    029      }
    030
    031      /** Returns the size of the AST <code>n</code> (see above),
    032        * except returns -1 if the size exceeds <code>limit</code>.
    033        **/
    034      //@ requires 0 <= limit;
    035      //@ ensures \result == -1 || (0 < \result && \result <= limit);
    036      public static int size(/*@ non_null */ ASTNode n, int limit) {
    037        if (limit == 0) {
    038          return -1;  // limit exceeded
    039        }
    040        int t = 1;  // count this node
    041        limit -= 1;
    042
    043        int k = n.childCount();
    044        // loop_invariant t + limit == METHOD_PRE(limit);
    045        // loop_invariant 0 < t && t <= METHOD_PRE(limit);
    046        //@ loop_invariant 0 <= limit;
    047        for (int i = 0; i < k; i++) {
    048          Object c = n.childAt(i);
    049
    050          int s;
    051          if (c instanceof ASTNode) {
    052            s = size((ASTNode)c, limit);
    053            if (s == -1) {
    054              return -1;  // limit exceeded while counting children
    055            }
    056          } else {
    057            if (limit == 0) {
    058              return -1;  // limit exceeded
    059            }
    060            s = 1;
    061          }
    062          //@ assert s <= limit;
    063          t += s;
    064          limit -= s;
    065        }
    066
    067        return t;
    068      }
    069    }