|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.AccessOp
de.uka.ilkd.key.logic.op.AttributeOp
All known Subclasses: de.uka.ilkd.key.logic.op.ShadowAttributeOp,
| AttributeOp | | public class AttributeOp extends AccessOp (Code) | | this class is used to represent the reference operator '.' of
Java, e.g.>> int[] a = new int[]{1,2,3}; int i = a.length; <<<
where the '.' in a.length points to field called length
ATTENTION: At this moment only variables are adressed to this may
change in future
|
| AttributeOp | | protected AttributeOp(IProgramVariable attribute)(Code) | | creates a new access operator for the given attribute
Parameters:
attribute - the ProgramVariable representing a field |
| arity | | public int arity()(Code) | | The arity of an attribute operator is 1 and the
corresponding subterm denotes the object whose attribute is
accessed.
arity of the Operator as int |
| attribute | | public IProgramVariable attribute()(Code) | | returns the attribute of the operator
the attribute of the operator |
| getAttributeOp | | public static AttributeOp getAttributeOp(IProgramVariable attribute)(Code) | | returns and if neccessary creates the access operator of the
given attribute
the attribute operator for the given attribute |
| getContainerType | | public KeYJavaType getContainerType()(Code) | | returns the KeYJavaType the attribute is declared in
|
| hashCode | | public int hashCode()(Code) | | |
| isShadowed | | public boolean isShadowed()(Code) | | true if the operator is a shadowed |
| referencePrefix | | public Term referencePrefix(Term t)(Code) | | the top level operator of t must be this
returns the reference prefix of this attribute of the given term
|
| sort | | public Sort sort()(Code) | | the sort of the attribute
|
| sort | | public Sort sort(Term[] term)(Code) | | determines the sort of the
Term if it would be created using this
Operator as top level operator and the given terms as sub terms. The
assumption that the constructed term would be allowed is not checked.
Parameters:
term - an array of Term containing the subterms of a (potential)term with this operator as top level operator sort of the term with this operator as top level operator of thegiven substerms |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | checks whether the top level structure of the given
Term is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator. The
assumption that the top level operator and the term are equal
is NOT checked.
true iff the top level structure ofthe @link Term is valid. |
|
|
|