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;
012:
013: import de.uka.ilkd.key.logic.Term;
014:
015: /**
016: *
017: */
018: public interface IUpdateOperator extends Operator, NonRigid {
019:
020: /**
021: * Replace the locations of this operator without changing anything else.
022: * This must not change the number of locations, i.e.
023: * <code>newLocs.length==locationCount()</code>
024: */
025: IUpdateOperator replaceLocations(Location[] newLocs);
026:
027: /**
028: * returns the array of location operators which are updated
029: */
030: ArrayOfLocation locationsAsArray();
031:
032: /**
033: * returns the number of locations
034: *
035: * @return the number of locations as int
036: */
037: int locationCount();
038:
039: /**
040: * returns the operator of <tt>n</tt>-th location
041: */
042: Location location(int n);
043:
044: /**
045: * returns the number of the subterm representing the value to which
046: * the locPos-th location is updated
047: */
048: int valuePos(int locPos);
049:
050: /**
051: * returns an array with all location positions of <code>loc</code>
052: *
053: * @param loc a n Operator accessing a location
054: * @return all location positions of <code>loc</code>
055: */
056: int[] getLocationPos(Operator loc);
057:
058: /**
059: * @return the index of the first subterm belonging to update entry
060: * <code>locPos</code>
061: */
062: int entryBegin(int locPos);
063:
064: /**
065: * @return the index after the last subterm belonging to update entry
066: * <code>locPos</code>. The entry is described within
067: * <tt>[entryBegin(i), entryEnd(i))</tt>
068: */
069: int entryEnd(int locPos);
070:
071: /**
072: * @return the index of the first subterm belonging to the location of entry
073: * <code>locPos</code>
074: */
075: int locationSubtermsBegin(int locPos);
076:
077: /**
078: * @return the index after the last subterm belonging to the location of
079: * update entry <code>locPos</code>. The location is described
080: * within
081: * <tt>[locationSubtermsBegin(i), locationSubtermsEnd(i))</tt>
082: */
083: int locationSubtermsEnd(int locPos);
084:
085: /**
086: * returns the n-th location of the update as term
087: *
088: * @param t
089: * Term with this operator as top level operator
090: * @param n
091: * an int specifying the position of the requested location
092: * @return the n-th location of term t updated by this operator
093: */
094: Term location(Term t, int n);
095:
096: /**
097: * returns value the n-th location is updated with
098: *
099: * @param t
100: * Term with this operator as top level operator
101: * @param n
102: * an int specifying the position of the location
103: * @return the value the n-th location is updated with
104: */
105: Term value(Term t, int n);
106:
107: /**
108: * @return the index of the subterm representing the formula/term the update
109: * is applied to
110: */
111: int targetPos();
112:
113: /**
114: * return the subterm representing the formula/term the update is applied to
115: *
116: * @param t
117: * Term with this operator as top level operator
118: * @return the target of this update application
119: */
120: Term target(Term t);
121:
122: }
|