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: //
09: //
10: package de.uka.ilkd.key.rule.metaconstruct;
11:
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.op.SVSubstitute;
15: import de.uka.ilkd.key.rule.MatchConditions;
16: import de.uka.ilkd.key.rule.inst.SVInstantiations;
17:
18: /** this class implements the interface for
19: * MetaAdderators. MetaAdderators are used to do complex term
20: * transformation when applying a taclet. Often these transformation
21: * caanot be described with the taclet scheme (or trying to do so would
22: * result in a huge number of rules)
23: */
24: public class MetaLength extends MetaField {
25:
26: public MetaLength() {
27: super ("#lengthReference");
28: }
29:
30: /** calculates the resulting term. */
31: public Term calculate(Term term, SVInstantiations svInst,
32: Services services) {
33: return termFactory.createAttributeTerm(services.getJavaInfo()
34: .getAttribute(
35: "length",
36: services.getJavaInfo().getKeYJavaType(
37: term.sub(0).sort())), term.sub(0));
38: }
39:
40: /** (non-Javadoc)
41: * by default meta operators do not match anything
42: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
43: */
44: public MatchConditions match(SVSubstitute subst,
45: MatchConditions mc, Services services) {
46: return null;
47: }
48:
49: }
|