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