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: package de.uka.ilkd.key.rule.conditions;
09:
10: import de.uka.ilkd.key.java.Services;
11: import de.uka.ilkd.key.java.abstraction.ClassType;
12: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
13: import de.uka.ilkd.key.logic.op.SVSubstitute;
14: import de.uka.ilkd.key.logic.op.SchemaVariable;
15: import de.uka.ilkd.key.rule.VariableConditionAdapter;
16: import de.uka.ilkd.key.rule.inst.SVInstantiations;
17:
18: /**
19: * This variable condition checks if a given type denotes an abstract class or
20: * interface type.
21: */
22: public class AbstractOrInterfaceType extends VariableConditionAdapter {
23:
24: private final TypeResolver resolver;
25: private final boolean negated;
26:
27: public AbstractOrInterfaceType(TypeResolver tr, boolean negation) {
28: this .resolver = tr;
29: this .negated = negation;
30: }
31:
32: public boolean check(SchemaVariable var,
33: SVSubstitute instCandidate, SVInstantiations instMap,
34: Services services) {
35: final KeYJavaType type = resolver.resolveType(var,
36: instCandidate, instMap, services);
37:
38: final boolean isClassType = type.getJavaType() instanceof ClassType;
39:
40: final boolean isAbstractOrInterface = isClassType
41: && ((ClassType) type.getJavaType()).isInterface()
42: || ((ClassType) type.getJavaType()).isAbstract();
43:
44: return negated ? !isAbstractOrInterface : isAbstractOrInterface;
45: }
46:
47: public String toString() {
48: String prefix = negated ? "\\not" : "";
49: return prefix + "\\isAbstractOrInterface (" + resolver + ")";
50: }
51:
52: }
|