001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    /* =========================================================================
004     * MethodSignature.java
005     * ========================================================================= */
006    
007    package javafe.reader;
008    
009    import java.util.*;
010    
011    import javafe.ast.*;
012    //@ model import javafe.util.Location;
013    
014    /* -------------------------------------------------------------------------
015     * MethodSignature
016     * ------------------------------------------------------------------------- */
017    
018    /**
019     * Represents the signature of a method in terms of AST elements.
020     */
021    
022    class MethodSignature
023    {
024      /* -- package instance methods ------------------------------------------- */
025    
026      /**
027       * Construct a new method signature with an empty sequence of parameter
028       * types and a void return type.
029       */
030      //@ requires classLocation != Location.NULL;
031      MethodSignature(int classLocation)
032      {
033        this.parameters = new Vector();
034        this.return_    = JavafePrimitiveType.make(TagConstants.VOIDTYPE, classLocation);
035    
036        //@ set parameters.elementType = \type(Type);
037        //@ set parameters.containsNull = false;
038      }
039    
040      /**
041       * Count the number of parameter types in this method signature.
042       * @return  the number of parameter types
043       */
044      //@ ensures \result>=0;
045      //@ ensures \result==parameters.elementCount;
046      int countParameters()
047      {
048        return parameters.size();
049      }
050    
051      /**
052       * Return a parameter type from this method signature.
053       * @param index  the index of the parameter type to return
054       * @return       the parameter type at index index
055       */
056      //@ requires 0<=index && index<parameters.elementCount;
057      //@ ensures \result != null;
058      //@ ensures \result.syntax;
059      Type parameterAt(int index)
060      {
061        return (Type)parameters.elementAt(index);
062      }    //@ nowarn Post;  // Unenforceable invariant on parameters
063    
064      /**
065       * Append a parameter type to this method signature.
066       * @param parameterType  the parameter type to append
067       */
068      //@ requires parameterType != null;
069      void appendParameter(Type parameterType)
070      {
071        parameters.addElement(parameterType);
072      }
073    
074      /**
075       * Return the return type of this method signature.
076       * @return  the return type
077       */
078      //@ ensures \result != null;
079      //@ ensures \result.syntax;
080      Type getReturn()
081      {
082        return return_;
083      }
084    
085      /**
086       * Change the return type of this method signature.
087       * @param return_  the new return type
088       */
089      //@ requires return_ != null;
090      //@ requires return_.syntax;
091      void setReturn(Type return_)
092      {
093        this.return_ = return_;
094      }
095    
096      /* -- private instance variables ----------------------------------------- */
097    
098      /**
099       * The parameter types of this method signature.
100       * Initialized by constructor.
101       */
102      //@ invariant parameters != null;
103      //@ invariant parameters.elementType == \type(Type);
104      //@ invariant !parameters.containsNull;
105      // Unenforceable invariant: contents are syntax
106      /*@spec_public*/ private Vector parameters;
107    
108      /**
109       * The return type of this method signature.
110       * Initialized by constructor.
111       */
112      //@ invariant return_ != null;
113      //@ invariant return_.syntax;
114      //@ spec_public
115      private Type return_;
116    
117    }
118