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:
011: package de.uka.ilkd.key.logic;
012:
013: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
014: import de.uka.ilkd.key.logic.op.Op;
015: import de.uka.ilkd.key.logic.op.Operator;
016:
017: /*
018: * A ProgramTerm represents a term with a modality operator like
019: * the diamond or box operator together with a JavaBlock. Instances
020: * should never be accessed via this interface, use the interface of
021: * the superclass Term and construct instances only via a TermFactory
022: * instead.
023: */
024:
025: class ProgramTerm extends Term {
026: /** the program
027: * @link aggregation
028: * @supplierCardinality 0..1
029: */
030: private final JavaBlock javaBlock;
031:
032: /** sub term */
033: private final ArrayOfTerm subTerm;
034:
035: /** caches depth */
036: private int depth = -1;
037:
038: /**
039: * creates a diamond term, so there is an additional
040: * parameter javaBlock
041: */
042: ProgramTerm(Operator modality, JavaBlock javaBlock, Term subTerm) {
043: this (modality, javaBlock, new Term[] { subTerm });
044: }
045:
046: ProgramTerm(Operator op, JavaBlock javaBlock, Term[] subTerm) {
047: super (op, op.sort(subTerm));
048: this .subTerm = new ArrayOfTerm(subTerm);
049: this .javaBlock = javaBlock;
050: fillCaches();
051: }
052:
053: /** @return n-th subterm (always the only one)*/
054: public Term sub(int n) {
055: return subTerm.getTerm(n);
056: }
057:
058: /** @return arity of the quantifier term 1 as int */
059: public int arity() {
060: return subTerm.size();
061: }
062:
063: /**@return depth of the term */
064: public int depth() {
065: if (this .depth == -1) {
066: int localdepth = 0;
067: for (int i = 0; i < subTerm.size(); i++) {
068: if (subTerm.getTerm(i).depth() > localdepth)
069: localdepth = subTerm.getTerm(i).depth();
070: }
071: this .depth = localdepth + 1;
072: }
073: return this .depth;
074: }
075:
076: /** @return JavaBlock if term has diamond */
077: public JavaBlock javaBlock() {
078: return javaBlock;
079: }
080:
081: /** @return an empty variable list */
082: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
083: return EMPTY_VAR_LIST;
084: }
085:
086: public String toString() {
087: StringBuffer sb = new StringBuffer();
088: if (op() == Op.DIA) {
089: sb.append("\\<").append(javaBlock).append("\\> ");
090: } else if (op() == Op.BOX) {
091: sb.append("\\[").append(javaBlock).append("\\] ");
092: } else if (op() == Op.TOUT) {
093: sb.append("\\[[").append(javaBlock).append("\\]] ");
094: } else {
095: // sb.append("???Some Strange Modality???").append(javaBlock);
096: sb.append("\\modality{" + op().name()).append("}").append(
097: javaBlock).append("\\endmodality ");
098: }
099: for (int i = 0; i < subTerm.size(); i++)
100: sb.append("(").append(subTerm.getTerm(i)).append(")");
101:
102: return sb.toString();
103: }
104:
105: }
|