| de.uka.ilkd.key.ProverFacade
ProverFacade | public interface ProverFacade (Code) | | |
Method Summary | |
void | doNotAddProgramVariables() | ProgramVariable | getAttribute(String name, KeYJavaType classReference) | Term | getAttributeTerm(ProgramVariable pvar, Term obj) | Function | getCollectionFunctionForFeature(String attr, Sort[] argSorts, Sort retSort) | JavaBlock | getConstructorCall(KeYJavaType cls, ProgramVariable result, ProgramVariable[] args) | Sort | getElementSortForCollectionSort(CollectionSort collSort) | KeYJavaType | getKeYJavaTypeForClass(String name) | KeYJavaType | getKeYJavaTypeForOCLBoolean() | KeYJavaType | getKeYJavaTypeForOCLInteger() | KeYJavaType | getKeYJavaTypeForOCLReal() | KeYJavaType | getKeYJavaTypeForOCLString() | JavaBlock | getMethodCall(ProgramVariable reference, String method, ProgramVariable result, ProgramVariable[] args) | JavaBlock | getMethodCall(ProgramVariable reference, String method, ProgramVariable result, ProgramVariable[] args, VarAndType[] excProgVars) | JavaBlock | getMethodCall(String method, ProgramVariable result, ProgramVariable[] args) | Term | getNullTerm() | Sort | getNumberSort() | ProgramVariable | getProgramVariable(String name, KeYJavaType s) | ProgramVariable | getProgramVariable(String name) | ProgramMethod | getQueryForFeature(String method, Term[] argterms) | Function | getRigidFunctionForFeature(String attr, Sort[] argSorts, Sort retSort) | Function | getRigidFunctionForStaticFeature(String attr, Sort enclosingClass, Sort retSort) | Sort | getSortForClass(String name) | Sort | getSortForOCLBag(NonCollectionSort elem) | Sort | getSortForOCLBoolean() | Sort | getSortForOCLInteger() | Sort | getSortForOCLReal() | Sort | getSortForOCLSequence(NonCollectionSort elem) | Sort | getSortForOCLSet(NonCollectionSort elem) | Sort | getSortForOCLString() | Sort | getSortForOCLType() | JavaBlock | getVoidMethodCall(ProgramVariable reference, String method, ProgramVariable[] args) | JavaBlock | getVoidMethodCall(ProgramVariable reference, String method, ProgramVariable[] args, VarAndType[] excProgVars) | JavaBlock | getVoidMethodCall(String method, ProgramVariable[] args) | boolean | isSortForClass(Sort s) | Services | services() |
doNotAddProgramVariables | void doNotAddProgramVariables()(Code) | | |
getSortForOCLBoolean | Sort getSortForOCLBoolean()(Code) | | |
getSortForOCLInteger | Sort getSortForOCLInteger()(Code) | | |
getSortForOCLString | Sort getSortForOCLString()(Code) | | |
isSortForClass | boolean isSortForClass(Sort s)(Code) | | |
|
|