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 de.uka.ilkd.key.java.Expression;
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
015: import de.uka.ilkd.key.java.expression.Literal;
016: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
017: import de.uka.ilkd.key.java.reference.ExecutionContext;
018: import de.uka.ilkd.key.logic.Name;
019: import de.uka.ilkd.key.logic.Namespace;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.TermFactory;
022: import de.uka.ilkd.key.logic.op.Function;
023: import de.uka.ilkd.key.util.Debug;
024: import de.uka.ilkd.key.util.ExtList;
025:
026: /** This class inherits from LDT and implements all method that are
027: * necessary to handle the primitive type boolean.
028: */
029: public class BooleanLDT extends LDT {
030:
031: /** the boolean literals as function symbols and terms */
032: private final Function bool_true;
033: private final Term term_bool_true;
034: private final Function bool_false;
035: private final Term term_bool_false;
036:
037: public BooleanLDT(Namespace sorts, Namespace functions) {
038: super (new Name("boolean"), sorts, PrimitiveType.JAVA_BOOLEAN);
039:
040: bool_true = addFunction((Function) functions.lookup(new Name(
041: "TRUE")));
042: term_bool_true = TermFactory.DEFAULT
043: .createFunctionTerm(bool_true);
044: bool_false = addFunction((Function) functions.lookup(new Name(
045: "FALSE")));
046: term_bool_false = TermFactory.DEFAULT
047: .createFunctionTerm(bool_false);
048: }
049:
050: /** returns true if the LDT is responsible for this kind of literals
051: * @param lit the Literal
052: * @return true if the LDT is responsible for this kind of literals
053: */
054: public boolean isResponsible(Literal lit) {
055: return (lit instanceof BooleanLiteral);
056: }
057:
058: /** returns true if the LDT offers an operation for the given java
059: * operator and the logic subterms
060: * @param op the de.uka.ilkd.key.java.expression.Operator to
061: * translate
062: * @param subs the logic subterms of the java operator
063: * @return true if the LDT offers an operation for the given java
064: * operator and the subterms
065: */
066: public boolean isResponsible(
067: de.uka.ilkd.key.java.expression.Operator op, Term[] subs,
068: Services services, ExecutionContext ec) {
069: if (subs.length == 1) {
070: return isResponsible(op, subs[0], services, ec);
071: } else if (subs.length == 2) {
072: return isResponsible(op, subs[0], subs[1], services, ec);
073: }
074: return false;
075: }
076:
077: /** returns true if the LDT offers an operation for the given
078: * binary java operator and the logic subterms
079: * @param op the de.uka.ilkd.key.java.expression.Operator to
080: * translate
081: * @param left the left subterm of the java operator
082: * @param right the right subterm of the java operator
083: * @return true if the LDT offers an operation for the given java
084: * operator and the subterms
085: */
086: public boolean isResponsible(
087: de.uka.ilkd.key.java.expression.Operator op, Term left,
088: Term right, Services services, ExecutionContext ec) {
089: return false;
090:
091: }
092:
093: /** returns true if the LDT offers an operation for the given
094: * unary java operator and the logic subterms
095: * @param op the de.uka.ilkd.key.java.expression.Operator to
096: * translate
097: * @param sub the logic subterms of the java operator
098: * @return true if the LDT offers an operation for the given java
099: * operator and the subterm
100: */
101: public boolean isResponsible(
102: de.uka.ilkd.key.java.expression.Operator op, Term sub,
103: Services services, ExecutionContext ec) {
104: return false;
105: }
106:
107: /** translates a given literal to its logic counterpart
108: * @param lit the Literal to be translated
109: * @return the Term that represents the given literal in its logic
110: * form
111: */
112: public Term translateLiteral(Literal lit) {
113: if (lit instanceof BooleanLiteral) {
114: return (((BooleanLiteral) lit).getValue() ? term_bool_true
115: : term_bool_false);
116: }
117: Debug.fail("booleanLDT: Wrong literal", lit);
118: return null;
119: }
120:
121: /** returns the function symbol for the given operation
122: * @return the function symbol for the given operation
123: */
124: public Function getFunctionFor(
125: de.uka.ilkd.key.java.expression.Operator op,
126: Services services, ExecutionContext ec) {
127: return null;
128: }
129:
130: public Term getFalseTerm() {
131: return term_bool_false;
132: }
133:
134: public Term getTrueTerm() {
135: return term_bool_true;
136: }
137:
138: /**
139: * returns the function representing the boolean value <tt>FALSE</tt>
140: * @return the function representing the boolean value <tt>FALSE</tt>
141: */
142: public Function getFalseConst() {
143: return bool_false;
144: }
145:
146: /**
147: * returns the function representing the boolean value <tt>TRUE</tt>
148: * @return the function representing the boolean value <tt>TRUE</tt>
149: */
150: public Function getTrueConst() {
151: return bool_true;
152: }
153:
154: public boolean hasLiteralFunction(Function f) {
155: return containsFunction(f) && f.arity() == 0;
156: }
157:
158: public Expression translateTerm(Term t, ExtList children) {
159: if (t.op() == bool_true)
160: return BooleanLiteral.TRUE;
161: if (t.op() == bool_false)
162: return BooleanLiteral.FALSE;
163: throw new RuntimeException(
164: "BooleanLDT: Cannot convert term to program: " + t);
165: }
166: }
|