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: package de.uka.ilkd.key.logic.op;
10:
11: import de.uka.ilkd.key.logic.sort.Sort;
12:
13: /**
14: * Operators implementing this interface may stand for
15: * locations as well. This means e.g. occur as top level operators on the
16: * left side of an assignment pair of an update.
17: */
18: public interface Location extends Operator, NonRigid {
19: /**
20: * Checks if location <code>loc</code> may be an alias of the current
21: * location.
22: * The <code>mayBeAliasOf</code> relation is <strong>not</strong> necessary
23: * symmetric as e.g. for attributes and their shadowed variant.
24: * @param loc the Location to check
25: * @return true if <code>loc</loc> may be an alias of the current operator
26: */
27: boolean mayBeAliasedBy(Location loc);
28:
29: /**
30: * returns the sort of the location
31: */
32: Sort sort();
33: }
|