001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.java.VarAndType;
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.logic.JavaBlock;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.op.Function;
019: import de.uka.ilkd.key.logic.op.ProgramMethod;
020: import de.uka.ilkd.key.logic.op.ProgramVariable;
021: import de.uka.ilkd.key.logic.sort.CollectionSort;
022: import de.uka.ilkd.key.logic.sort.NonCollectionSort;
023: import de.uka.ilkd.key.logic.sort.Sort;
024:
025: public interface ProverFacade {
026:
027: Sort getSortForClass(String name);
028:
029: boolean isSortForClass(Sort s);
030:
031: Sort getNumberSort();
032:
033: Sort getSortForOCLInteger();
034:
035: Sort getSortForOCLReal();
036:
037: Sort getSortForOCLString();
038:
039: Sort getSortForOCLBoolean();
040:
041: KeYJavaType getKeYJavaTypeForOCLInteger();
042:
043: KeYJavaType getKeYJavaTypeForOCLReal();
044:
045: KeYJavaType getKeYJavaTypeForOCLString();
046:
047: KeYJavaType getKeYJavaTypeForOCLBoolean();
048:
049: KeYJavaType getKeYJavaTypeForClass(String name);
050:
051: Sort getSortForOCLType();
052:
053: Sort getElementSortForCollectionSort(CollectionSort collSort);
054:
055: Sort getSortForOCLSet(NonCollectionSort elem);
056:
057: Sort getSortForOCLSequence(NonCollectionSort elem);
058:
059: Sort getSortForOCLBag(NonCollectionSort elem);
060:
061: // ProgramVariable getProgramVariable(String name,Sort s);
062: ProgramVariable getProgramVariable(String name, KeYJavaType s);
063:
064: ProgramVariable getProgramVariable(String name);
065:
066: void doNotAddProgramVariables();
067:
068: Function getRigidFunctionForFeature(String attr, Sort[] argSorts,
069: Sort retSort);
070:
071: Function getRigidFunctionForStaticFeature(String attr,
072: Sort enclosingClass, Sort retSort);
073:
074: ProgramMethod getQueryForFeature(String method, Term[] argterms);
075:
076: JavaBlock getMethodCall(ProgramVariable reference, String method,
077: ProgramVariable result, ProgramVariable[] args);
078:
079: JavaBlock getMethodCall(ProgramVariable reference, String method,
080: ProgramVariable result, ProgramVariable[] args,
081: VarAndType[] excProgVars);
082:
083: JavaBlock getVoidMethodCall(ProgramVariable reference,
084: String method, ProgramVariable[] args);
085:
086: JavaBlock getVoidMethodCall(ProgramVariable reference,
087: String method, ProgramVariable[] args,
088: VarAndType[] excProgVars);
089:
090: JavaBlock getMethodCall(String method, ProgramVariable result,
091: ProgramVariable[] args);
092:
093: JavaBlock getVoidMethodCall(String method, ProgramVariable[] args);
094:
095: JavaBlock getConstructorCall(KeYJavaType cls,
096: ProgramVariable result, ProgramVariable[] args);
097:
098: Function getCollectionFunctionForFeature(String attr,
099: Sort[] argSorts, Sort retSort);
100:
101: Services services();
102:
103: Term getNullTerm();
104:
105: ProgramVariable getAttribute(String name, KeYJavaType classReference);
106:
107: Term getAttributeTerm(ProgramVariable pvar, Term obj);
108:
109: }
|