001    package escjava.vcGeneration;
002    
003    import java.util.Vector;
004    
005    import java.lang.ArrayIndexOutOfBoundsException;
006    
007    abstract public class TFunction extends TNode {
008    
009        /*
010         * This field is not protected because we can remove childs
011         * in TProofSimplifier.java
012         */
013        /*@ non_null @*/public Vector sons = new Vector();
014    
015        /*@
016         @ ensures \old(sons.size()) == sons.size()-1;
017         @*/
018        void addSon(/*@ non_null @*/TNode n) {
019            sons.add(n);
020    
021            //++
022            if (n.parent != null)
023                TDisplay.err(this, "addSon", "node already have a parent");
024            //++
025            else
026                n.parent = this;
027        }
028    
029        /*@
030         @ ensures index >= 0 && index <= sons.size()-1;
031         @*/
032        public TNode getChildAt(int index) {
033            try {
034                return (TNode) sons.elementAt(index);
035            } catch (ArrayIndexOutOfBoundsException e) {
036                TDisplay.err(this, "getChildAt", "ArrayIndexOutOfBoundsException"
037                        + e.getMessage());
038                return null; /* notice this default behaviour */
039            }
040        }
041    
042        protected void typeTree() {
043    
044            /* recursive call on the sons */
045            for (int i = 0; i <= sons.size() - 1; i++)
046                getChildAt(i).typeTree();
047    
048        }
049    
050    }