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: package de.uka.ilkd.key.jml;
011:
012: import java.util.LinkedHashMap;
013:
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.statement.LoopStatement;
016: import de.uka.ilkd.key.logic.SetAsListOfLocationDescriptor;
017: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
018: import de.uka.ilkd.key.logic.Term;
019: import de.uka.ilkd.key.logic.TermBuilder;
020: import de.uka.ilkd.key.logic.op.Op;
021: import de.uka.ilkd.key.logic.op.ProgramVariable;
022:
023: public class LoopInvariant extends JMLSpec implements AssignableSpec {
024:
025: private Services services;
026:
027: // contains an assignable keyword (like nothing, everithing, ...),
028: // if one occurd in the specification.
029: private String assignableMode = null;
030: protected SetOfLocationDescriptor assignableLocations = SetAsListOfLocationDescriptor.EMPTY_SET;
031:
032: private LoopStatement loop;
033:
034: private Term variant = null;
035: private Term invariant = null;
036:
037: //post condition for loop. Only used by VBT specific rules.
038: private Term post;
039:
040: private LinkedHashMap term2old;
041:
042: private TermBuilder df = TermBuilder.DF;
043:
044: private final ProgramVariable selfVar;
045:
046: public LoopInvariant(LoopStatement loop, Services services,
047: ProgramVariable selfVar) {
048: this .services = services;
049: post = invariant = df.tt();
050: this .loop = loop;
051: this .term2old = new LinkedHashMap();
052: this .selfVar = selfVar;
053: }
054:
055: public void addInvariant(Term t) {
056: invariant = df.and(invariant, t);
057: }
058:
059: public void setVariant(Term t) {
060: variant = t;
061: }
062:
063: public Term getInvariant() {
064: return invariant;
065: }
066:
067: public Term getVariant() {
068: return variant;
069: }
070:
071: public LoopStatement getLoop() {
072: return loop;
073: }
074:
075: public void register() {
076: services.getImplementation2SpecMap().addLoopSpec(this );
077: }
078:
079: public void addAssignable(SetOfLocationDescriptor locations) {
080: assignableLocations = assignableLocations.union(locations);
081: }
082:
083: public SetOfLocationDescriptor getAssignable() {
084: return assignableLocations;
085: }
086:
087: public void setAssignableMode(String s) {
088: assignableMode = s;
089: }
090:
091: public LinkedHashMap getTerm2Old() {
092: return term2old;
093: }
094:
095: public void addPost(Term t) {
096: if (t != null) {
097: post = tf.createJunctorTermAndSimplify(Op.AND, post, t);
098: }
099: }
100:
101: public Term getPost() {
102: return post;
103: }
104:
105: public String getAssignableMode() {
106: if (assignableLocations.size() == 0 && assignableMode == null) {
107: return "everything";
108: }
109: // an inconsistent case
110: if (assignableLocations.size() > 0
111: && "nothing".equals(assignableMode)) {
112: return null;
113: }
114: return assignableMode;
115: }
116:
117: public ProgramVariable getSelfVar() {
118: return selfVar;
119: }
120:
121: }
|