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    }