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: package de.uka.ilkd.key.logic.ldt;
011:
012: import java.util.HashMap;
013:
014: import de.uka.ilkd.key.java.Expression;
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.abstraction.*;
017: import de.uka.ilkd.key.java.expression.Literal;
018: import de.uka.ilkd.key.java.reference.ExecutionContext;
019: import de.uka.ilkd.key.logic.Name;
020: import de.uka.ilkd.key.logic.Named;
021: import de.uka.ilkd.key.logic.Namespace;
022: import de.uka.ilkd.key.logic.Term;
023: import de.uka.ilkd.key.logic.op.Function;
024: import de.uka.ilkd.key.logic.sort.Sort;
025: import de.uka.ilkd.key.rule.SetAsListOfTaclet;
026: import de.uka.ilkd.key.rule.SetOfTaclet;
027: import de.uka.ilkd.key.util.ExtList;
028:
029: /** this class extends the class ADT and is used to represent language
030: * datatype models e.g. a model for the java type int, boolean etc.
031: * It contains the necessary function symbols, sorts and Taclets. The
032: * class TypeConverter needs this class to convert java-program
033: * constructs to logic terms.
034: */
035: public abstract class LDT extends ADT {
036:
037: /** the function namespace */
038: private Namespace functions = new Namespace();
039:
040: /** the model specific rules */
041: private SetOfTaclet rules = SetAsListOfTaclet.EMPTY_SET;
042:
043: /** the sort represented by the LDT */
044: protected final Sort sort;
045:
046: /**
047: * one LDT may model several program types; this is the list
048: * of these types
049: */
050: protected final Type type;
051:
052: protected HashMap keyJavaType = new HashMap();
053:
054: /**
055: * creates a new LDT complete with the target sort of the language
056: * datatype, the java datatype, and sorts
057: * @param name the name of the language datatype model and the
058: * corresponding sort
059: * @param sorts namespace which contains the target sort
060: * @param type the type used in the java program esp. in the AST
061: * of the java program
062: */
063: public LDT(Name name, Namespace sorts, Type type) {
064: super (name);
065: this .sort = (Sort) sorts.lookup(name);
066: this .type = type;
067: assert sort != null;
068: addSort(sort);
069: keyJavaType.put(type, new KeYJavaType(type, sort));
070: }
071:
072: /**
073: * adds a function to the LDT
074: * @return the added function (for convenience reasons)
075: */
076: public Function addFunction(Function f) {
077: functions.add(f);
078: return f;
079: }
080:
081: /**
082: * looks up a function in the namespace and add it to the LDT
083: * @param functions a Namespace with symbols
084: * @param String the String with the name of the function to look up
085: * @return the added function (for convenience reasons)
086: */
087: public Function addFunction(Namespace funcNS, String funcName) {
088: final Function f = (Function) funcNS.lookup(new Name(funcName));
089: functions.add(f);
090: if (f == null) {
091: System.out.println("IntegerLDT: Function " + funcName
092: + " not found");
093: }
094: return f;
095: }
096:
097: /** returns the sort the java type is mapped to
098: * @return the sort the java type is mapped to
099: */
100: public Sort targetSort() {
101: return sort;
102: }
103:
104: /** returns the java type the model describes
105: * @return the java type the model describes
106: */
107: public Type javaType() {
108: return type;
109: }
110:
111: /** returns the KeYJavaType for the the given type
112: * @param t the Type for which the coressponding KeYJavaType has to be
113: * returned
114: * @return the KeYJavaType the the given type t
115: */
116: public KeYJavaType getKeYJavaType(Type t) {
117: return (KeYJavaType) keyJavaType.get(t);
118: }
119:
120: /** returns the basic functions of the model
121: * @return the basic functions of the model
122: */
123: public Namespace functions() {
124: return functions;
125: }
126:
127: /** returns the model specific rules
128: * @return the model specific rules
129: */
130: public SetOfTaclet rules() {
131: return rules;
132: }
133:
134: /** toString */
135: public String toString() {
136: return "LDT " + name() + " (" + targetSort() + "<->"
137: + javaType() + ")";
138: }
139:
140: /** returns the file ID for the parser */
141: public String getFile() {
142: return name().toString();
143: }
144:
145: /** returns true if the LDT offers an operation for the given java
146: * operator and the logic subterms
147: * @param op the de.uka.ilkd.key.java.expression.Operator to
148: * translate
149: * @param subs the logic subterms of the java operator
150: * @param services the Services
151: * @param ec the ExecutionContext in which the expression is evaluated
152: * @return true if the LDT offers an operation for the given java
153: * operator and the subterms
154: */
155: public abstract boolean isResponsible(
156: de.uka.ilkd.key.java.expression.Operator op, Term[] subs,
157: Services services, ExecutionContext ec);
158:
159: /** returns true if the LDT offers an operation for the given
160: * binary java operator and the logic subterms
161: * @param op the de.uka.ilkd.key.java.expression.Operator to
162: * translate
163: * @param left the left subterm of the java operator
164: * @param right the right subterm of the java operator
165: * @param services the Services
166: * @param ec the ExecutionContext in which the expression is evaluated
167: * @return true if the LDT offers an operation for the given java
168: * operator and the subterms
169: */
170: public abstract boolean isResponsible(
171: de.uka.ilkd.key.java.expression.Operator op, Term left,
172: Term right, Services services, ExecutionContext ec);
173:
174: /** returns true if the LDT offers an operation for the given
175: * unary java operator and the logic subterms
176: * @param op the de.uka.ilkd.key.java.expression.Operator to
177: * translate
178: * @param sub the logic subterms of the java operator
179: * @param services the Services
180: * @param ec the ExecutionContext in which the expression is evaluated * @param services TODO
181: * @return true if the LDT offers an operation for the given java
182: * operator and the subterm
183: */
184: public abstract boolean isResponsible(
185: de.uka.ilkd.key.java.expression.Operator op, Term sub,
186: Services services, ExecutionContext ec);
187:
188: /** translates a given literal to its logic counterpart
189: * @param lit the Literal to be translated
190: * @return the Term that represents the given literal in its logic
191: * form
192: */
193: public abstract Term translateLiteral(Literal lit);
194:
195: /** returns the function symbol for the given operation
196: * @return the function symbol for the given operation
197: */
198: public abstract Function getFunctionFor(
199: de.uka.ilkd.key.java.expression.Operator op, Services serv,
200: ExecutionContext ec);
201:
202: public boolean containsFunction(Function op) {
203: Named n = functions.lookup(op.name());
204: return (n == op);
205: }
206:
207: public abstract boolean hasLiteralFunction(Function f);
208:
209: public abstract Expression translateTerm(Term t, ExtList children);
210:
211: }
|