    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_    = PrimitiveType.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