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 }