01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: //
17:
18: package de.uka.ilkd.key.proof.decproc.translation;
19:
20: import org.apache.log4j.Logger;
21: import de.uka.ilkd.key.logic.op.Operator;
22:
23: /** This class represents the translation rule for <tt>Operator</tt>s of unknown or unexpected classes.
24: * <p>
25: * It only throws an <tt>Exception</tt> to indicate the occurrence of this <tt>Operator</tt>
26: *
27: * @author akuwertz
28: * @version 1.0, 04/03/2006
29: */
30:
31: public class TranslateUnknownOp implements IOperatorTranslation {
32:
33: /* Additional fields */
34:
35: /** A <tt>Logger</tt> for logging and debugging operator translation */
36: private static final Logger logger = Logger
37: .getLogger(TranslateUnknownOp.class.getName());
38: // Logger is created hierarchical to inherit configuration and behaviour from parent
39:
40: /** String constant for error message */
41: private static final String unknownOp = "Unknown operator occurred and could not be translated! Operator is instance of class: ";
42:
43: /* Public method implementation*/
44:
45: /* (non-Javadoc)
46: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#isApplicable(de.uka.ilkd.key.logic.op.Operator)
47: */
48: public boolean isApplicable(Operator op) {
49: return true;
50: }
51:
52: /* (non-Javadoc)
53: * @see de.uka.ilkd.key.proof.decproc.translation.IOperatorTranslation#translate(de.uka.ilkd.key.logic.op.Operator, de.uka.ilkd.key.proof.decproc.translation.TermTranslationVisitor)
54: */
55: public Object translate(Operator op,
56: TermTranslationVisitor ttVisitor) {
57: logger.info("Found unexpected or unknown operator!");
58: logger.info("Stopping translation of current term!");
59: throw new IllegalArgumentException(unknownOp + op.getClass());
60: }
61: }
|