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.rule.inst;
012:
013: import de.uka.ilkd.key.java.ProgramElement;
014: import de.uka.ilkd.key.java.reference.ExecutionContext;
015: import de.uka.ilkd.key.logic.PosInProgram;
016:
017: /**
018: * this class is created if the scheme given by a context term has
019: * matched to a java program. The ContextStatementBlockInstantiation class
020: * stores the instantiations of the prefix and the suffix.
021: */
022: public class ContextStatementBlockInstantiation {
023:
024: /** the end position of the prefix omega */
025: private PosInProgram prefixEnd;
026:
027: /** the start position of the suffix omega */
028: private PosInProgram suffixStart;
029:
030: /** the execution context of the first active statement */
031: private ExecutionContext activeStatementContext;
032:
033: /** the whole program element this context term inst refers to */
034: private ProgramElement programElement;
035:
036: /** creates a ContextStatementBlockInstantiation of a context term
037: * @param prefixEnd the PosInProgram describing the first
038: * statement after the end of the prefix
039: * @param suffixStart the PosInProgram describing the statement
040: * just before the suffix begins
041: * @param activeStatementContext the ExecutionContext of the first
042: * active statement
043: * @param pe the ProgramElement the context positions are related to
044: */
045: public ContextStatementBlockInstantiation(PosInProgram prefixEnd,
046: PosInProgram suffixStart,
047: ExecutionContext activeStatementContext, ProgramElement pe) {
048:
049: this .prefixEnd = prefixEnd;
050: this .suffixStart = suffixStart;
051: this .activeStatementContext = activeStatementContext;
052: this .programElement = pe;
053: }
054:
055: /** returns the end position of the prefix
056: * @return the end position of the prefix
057: */
058: public PosInProgram prefix() {
059: return prefixEnd;
060: }
061:
062: /**
063: * returns the PosInProgram describing
064: * the statement just before the suffix begins
065: */
066: public PosInProgram suffix() {
067: return suffixStart;
068: }
069:
070: /**
071: * returns the execution context of the first active statement or
072: * null if match is performed outer most
073: */
074: public ExecutionContext activeStatementContext() {
075: return activeStatementContext;
076: }
077:
078: /**
079: * returns the program element this context term instantiation refers to
080: * @return returns the program element this context term instantiation
081: * refers to
082: */
083: public ProgramElement programElement() {
084: return programElement;
085: }
086:
087: public boolean equals(Object o) {
088: if (!(o instanceof ContextStatementBlockInstantiation)) {
089: return false;
090: }
091: final ContextStatementBlockInstantiation inst = (ContextStatementBlockInstantiation) o;
092: if (prefixEnd == null && inst.prefixEnd != null)
093: return false;
094: if (suffixStart == null && inst.suffixStart != null)
095: return false;
096: if (activeStatementContext == null
097: && inst.activeStatementContext != null)
098: return false;
099: if (programElement == null && inst.programElement != null)
100: return false;
101:
102: if (!suffixStart.equals(inst.suffixStart))
103: return false;
104: if (!prefixEnd.equals(inst.prefixEnd))
105: return false;
106:
107: if (!activeStatementContext.equals(inst.activeStatementContext))
108: return false;
109:
110: if (!(programElement.equals(inst.programElement)))
111: return false;
112:
113: return true;
114: }
115:
116: public int hashCode() {
117: int hashCode = 1;
118: if (prefixEnd != null) {
119: hashCode = 17 * prefixEnd.hashCode();
120: }
121: if (suffixStart != null) {
122: hashCode += 17 * suffixStart.hashCode();
123: }
124: if (activeStatementContext != null) {
125: hashCode += 17 * activeStatementContext.hashCode();
126: }
127: if (programElement != null) {
128: hashCode += 17 * programElement.hashCode();
129: }
130: return hashCode;
131: }
132:
133: /** toString */
134: public String toString() {
135: String result = "ContextStatementBlockInstantiation:\n";
136: result += "Prefix ends before " + prefixEnd.toString();
137: result += "\nSuffix starts after " + suffixStart.toString();
138: result += "\nFirst active statement has execution context "
139: + activeStatementContext;
140: result += "\nRefers to Program " + programElement;
141: return result + "\n";
142: }
143: }
|