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.op.oclop;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.op.TermSymbol;
016: import de.uka.ilkd.key.logic.sort.Sort;
017: import de.uka.ilkd.key.logic.sort.oclsort.CollectionSort;
018: import de.uka.ilkd.key.logic.sort.oclsort.OclSort;
019:
020: /**
021: * Represents the OCL operation: iterate()
022: */
023: public class OclIterate extends TermSymbol {
024:
025: public OclIterate() {
026: super (new Name("$iterate"), null);
027: }
028:
029: /** @return arity of the Function as int */
030: public int arity() {
031: return 3;
032: }
033:
034: /**
035: * checks if the given term is syntactically valid at its top
036: * level assumed the top level operator were this, i.e. if the
037: * direct subterms can be subterms of a term with this top level
038: * operator, the method returns true. Furthermore, it is checked
039: * that no variables are bound for none of the subterms.
040: * @param term the Term to be checked.
041: * @return true iff the given term has
042: * subterms that are suitable for this function.
043: */
044: public boolean validTopLevel(Term term) {
045: if (term.arity() != arity()) {
046: return false;
047: }
048: if (term.varsBoundHere(0).size() != 0
049: || term.varsBoundHere(1).size() != 0
050: || term.varsBoundHere(2).size() != 2) {
051: return false;
052: }
053: if (!(term.sub(0).sort() instanceof CollectionSort)) {
054: return false;
055: }
056: CollectionSort collSort = (CollectionSort) term.sub(0).sort();
057: Sort iterVariableSort = term.varsBoundHere(2)
058: .getQuantifiableVariable(0).sort();
059: Sort accVariableSort = term.varsBoundHere(2)
060: .getQuantifiableVariable(1).sort();
061: Sort initAccValueSort = term.sub(1).sort();
062: Sort exprSort = term.sub(2).sort();
063: if (!collSort.getElemSort().extendsTrans(iterVariableSort)) {
064: return false;
065: }
066: if (!initAccValueSort.extendsTrans(accVariableSort)) {
067: return false;
068: }
069: if (!exprSort.extendsTrans(accVariableSort)) {
070: return false;
071: }
072: return true;
073: }
074:
075: public Sort sort(Term[] subTerm) {
076: if (subTerm.length != arity()) {
077: throw new IllegalArgumentException(
078: "Cannot determine sort of "
079: + "invalid term (Wrong arity).");
080: }
081: if (!(subTerm[0].sort() instanceof CollectionSort)) {
082: throw new IllegalArgumentException(
083: "Cannot determine sort of "
084: + "invalid term (First argument must be a Collection).");
085: }
086: return subTerm[2].sort();
087: }
088:
089: public String toString() {
090: return (name() + ":" + OclSort.OCLGENERIC);
091: }
092:
093: public String proofToString() {
094: String s = OclSort.OCLGENERIC + " " + name();
095: s += "(" + OclSort.COLLECTION_OF_OCLANY + ","
096: + OclSort.OCLGENERIC + "," + OclSort.OCLGENERIC;
097: s += ");\n";
098: return s;
099: }
100: }
|