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: package de.uka.ilkd.key.rule.updatesimplifier;
010:
011: import de.uka.ilkd.key.logic.Term;
012: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
013: import de.uka.ilkd.key.logic.op.Location;
014: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
015:
016: /**
017: * Models an assignment pair <code> l_i := t_i </code> of an update.
018: * This data structure is only used for update simplification.
019: */
020: public interface AssignmentPair {
021:
022: /**
023: * TODO: should guards and bound variables also be compared here???
024: */
025: public static class LocationAsKey {
026: final AssignmentPair pair;
027:
028: public LocationAsKey(AssignmentPair pair) {
029: this .pair = pair;
030: }
031:
032: public int hashCode() {
033: return pair.locationHashCode();
034: }
035:
036: public boolean equals(Object o) {
037: if (!(o instanceof LocationAsKey))
038: return false;
039: return pair.equalLocations(((LocationAsKey) o).pair);
040: }
041:
042: public AssignmentPair getAssignmentPair() {
043: return pair;
044: }
045: }
046:
047: /**
048: * returns the location
049: * @return the left side of the assignment
050: */
051: Term locationAsTerm();
052:
053: /**
054: * returns the location operator
055: * @return the location specifying operator
056: */
057: Location location();
058:
059: /**
060: * returns the locations sub terms
061: * @return the left side of the assignment
062: */
063: Term[] locationSubs();
064:
065: /**
066: * returns the value that is assigned to the location and adds
067: * if necessary (i.e. the static type <code>T</code> of the location as term is not a
068: * supersort) a type cast <code> (T) </code> in front.
069: * @return the right side of the assignment
070: */
071: Term value();
072:
073: /**
074: * returns the value that is assigned to the location
075: * without adding any cast. Use this method with care.
076: * @return the right side of the assignment
077: */
078: Term valueUnsafe();
079:
080: /**
081: * The guard this update might have. This returns the formula <tt>true</tt>
082: * in case of an unguarded assignment
083: */
084: Term guard();
085:
086: /**
087: * If this returns <code>true</code> then one cannot assume that the guard
088: * is valid (always true)
089: */
090: boolean nontrivialGuard();
091:
092: /**
093: * Variables that be used to express parallel execution of
094: * unboundedly/infinitely many updates
095: *
096: * @return variables that are bound for this assignment pair
097: */
098: ArrayOfQuantifiableVariable boundVars();
099:
100: /**
101: * @return the set of quantifiable variables that turn up free in this
102: * assignment pair
103: */
104: SetOfQuantifiableVariable freeVars();
105:
106: /**
107: * compares the location of the given assignment pair with the
108: * current location and returns true if they are equal
109: * @param p the AssignmentPair whose location is compared
110: * @return true if the location that is updated is equal to the location
111: * of the given assignment pair
112: */
113: boolean equalLocations(AssignmentPair p);
114:
115: /**
116: * TODO: must guards and bound variables also be considered at this point?
117: *
118: * returns an int fulfilling the usual hashcode properties but
119: * without consideration of the value part of the assignment pair
120: * @return an int as location hashcode
121: */
122: int locationHashCode();
123: }
|