de.uka.ilkd.key.logic.sort

Class ProgramSVSort.MethodNameSort

java.lang.Object

de.uka.ilkd.key.logic.sort.AbstractSort

de.uka.ilkd.key.logic.sort.ProgramSVSort

de.uka.ilkd.key.logic.sort.ProgramSVSort.MethodNameSort

All Implemented Interfaces:

Named, Sort

Enclosing class:

ProgramSVSort

private static class ProgramSVSort.MethodNameSort
extends ProgramSVSort

This sort represents a type of program schema variables that match on names of method references, i.e. the "m" of o.m(p1,pn). It can also be made to match only specific method names defined by the parameter "name".

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.logic.sort.ProgramSVSort

ProgramSVSort.SimpleExpressionNonStringObjectSort, ProgramSVSort.SimpleExpressionStringSort

Field Summary

Fields

Modifier and Type	Field and Description
private ProgramElementName	methodName

Fields inherited from class de.uka.ilkd.key.logic.sort.ProgramSVSort

ARRAYINITIALIZER, ARRAYLENGTH, ARRAYPOSTDECL, CATCH, CLASSREFERENCE, CONSTANT_PRIMITIVE_TYPE_VARIABLE, CONSTANT_STRING_VARIABLE, EXECUTIONCONTEXT, EXPRESSION, FORLOOP, FORUPDATES, GUARD, JAVABOOLEANEXPRESSION, LABEL, LEFTHANDSIDE, LOCALVARIABLE, LOOPINIT, METHODBODY, METHODNAME, MULTIPLEVARDECL, NEWARRAY, NONMODELMETHODBODY, NONSIMPLE_NEW, NONSIMPLEEXPRESSION, NONSIMPLEEXPRESSIONNOCLASSREFERENCE, NONSIMPLEMETHODREFERENCE, NONSTRINGLITERAL, PROGRAMMETHOD, SIMPLE_NEW, SIMPLEANYJAVANUMBERTYPEEXPRESSION, SIMPLEANYJAVATYPEEXPRESSION, SIMPLEANYNUMBERTYPEEXPRESSION, SIMPLEEXPRESSION, SIMPLEJAVABIGINTEXPRESSION, SIMPLEJAVABOOLEANEXPRESSION, SIMPLEJAVABYTEEXPRESSION, SIMPLEJAVABYTESHORTEXPRESSION, SIMPLEJAVABYTESHORTINTEXPRESSION, SIMPLEJAVACHARBYTESHORTINTEXPRESSION, SIMPLEJAVACHAREXPRESSION, SIMPLEJAVAINTEXPRESSION, SIMPLEJAVAINTLONGEXPRESSION, SIMPLEJAVALONGEXPRESSION, SIMPLEJAVASHORTEXPRESSION, SIMPLEJAVASHORTINTLONGEXPRESSION, SIMPLENONSTRINGOBJECTEXPRESSION, SIMPLESTRINGEXPRESSION, SPECIALCONSTRUCTORREFERENCE, STATEMENT, STATICVARIABLE, STRINGLITERAL, SWITCH, TYPE, TYPENOTPRIMITIVE, VARIABLE, VARIABLEINIT

Fields inherited from interface de.uka.ilkd.key.logic.sort.Sort

ANY, CAST_NAME, EXACT_INSTANCE_NAME, FORMULA, INSTANCE_NAME, TERMLABEL, UPDATE

Constructor Summary

Constructors

Constructor and Description
MethodNameSort()
MethodNameSort(ProgramElementName name)

Method Summary

Modifier and Type	Method and Description
protected boolean	canStandFor(ProgramElement pe, Services services)
ProgramSVSort	createInstance(java.lang.String parameter)
java.lang.String	declarationString()

Methods inherited from class de.uka.ilkd.key.logic.sort.ProgramSVSort

canStandFor, canStandFor, getKeYJavaType, getSVWithSort, implicit, methodConstrReference, name2sort

Methods inherited from class de.uka.ilkd.key.logic.sort.AbstractSort

extendsSorts, extendsSorts, extendsTrans, getCastSymbol, getExactInstanceofSymbol, getInstanceofSymbol, isAbstract, name, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

methodName

private final ProgramElementName methodName

Constructor Detail

MethodNameSort

public MethodNameSort()

MethodNameSort

public MethodNameSort(ProgramElementName name)

Method Detail

canStandFor

protected boolean canStandFor(ProgramElement pe,
                              Services services)

Specified by:

canStandFor in class ProgramSVSort

createInstance

public ProgramSVSort createInstance(java.lang.String parameter)

Overrides:

createInstance in class ProgramSVSort

declarationString

public java.lang.String declarationString()

Specified by:

declarationString in interface Sort

Overrides:

declarationString in class AbstractSort