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.java.annotation;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.visitor.Visitor;
015: import de.uka.ilkd.key.logic.ArrayOfTerm;
016: import de.uka.ilkd.key.logic.IteratorOfLocationDescriptor;
017: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
018: import de.uka.ilkd.key.logic.SetAsListOfLocationDescriptor;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.op.ProgramVariable;
021:
022: public class LoopInvariantAnnotation implements Annotation {
023:
024: private final Term invariant;
025: private final Term variant;
026: private final Term post;
027: private final SetOfLocationDescriptor assignable;
028: // array containing terms at indices 2n and program variables for
029: // storing the initial values of these terms at indices 2n+1
030: // (for 0<=n<olds.size()/2).
031: private final ArrayOfTerm olds;
032: private final ProgramVariable selfVar;
033:
034: public LoopInvariantAnnotation(Term invariant,
035: SetOfLocationDescriptor assignable, ArrayOfTerm olds,
036: Term variant, Term post, ProgramVariable selfVar) {
037: this .invariant = invariant;
038: this .variant = variant;
039: this .post = post;
040: this .assignable = assignable == null ? SetAsListOfLocationDescriptor.EMPTY_SET
041: : assignable;
042: this .olds = olds == null ? new ArrayOfTerm() : olds;
043: this .selfVar = selfVar;
044: }
045:
046: public Term invariant() {
047: return invariant;
048: }
049:
050: public Term variant() {
051: return variant;
052: }
053:
054: public Term post() {
055: return post;
056: }
057:
058: public SetOfLocationDescriptor assignable() {
059: return assignable;
060: }
061:
062: public ArrayOfTerm olds() {
063: return olds;
064: }
065:
066: public ProgramVariable getSelfVar() {
067: return selfVar;
068: }
069:
070: public String toString() {
071: String result = "invariant: " + invariant + "\nvariant: "
072: + variant + "\nassignable: ";
073: IteratorOfLocationDescriptor it = assignable.iterator();
074: while (it.hasNext()) {
075: result += " " + it.next();
076: }
077: result += "\nold: " + olds;
078: for (int i = 0; i < olds.size(); i++) {
079: result += olds.getTerm(i) + (i % 2 == 0 ? "=" : " ");
080: }
081: return result;
082: }
083:
084: public SourceElement getFirstElement() {
085: return null;
086: }
087:
088: public SourceElement getLastElement() {
089: return null;
090: }
091:
092: public Position getStartPosition() {
093: return null;
094: }
095:
096: public Position getEndPosition() {
097: return null;
098: }
099:
100: public Position getRelativePosition() {
101: return null;
102: }
103:
104: public PositionInfo getPositionInfo() {
105: return null;
106: }
107:
108: public void visit(Visitor v) {
109: // do nothing
110: }
111:
112: public void prettyPrint(PrettyPrinter w) throws java.io.IOException {
113: // do nothing
114: }
115:
116: public boolean equalsModRenaming(SourceElement se,
117: NameAbstractionTable nat) {
118: return false;
119: }
120: }
|