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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.init;
019:
020: /**
021: * Describes which invariants are to be preselected (i.e. assumed by default),
022: * and for which ones an insertion rule is created which allows the user to
023: * select them when needed.
024: */
025: public abstract class InvariantSelectionStrategy {
026:
027: /**
028: * A strategy which preselects all invariants.
029: */
030: public final static InvariantSelectionStrategy PRESELECT_ALL = new InvariantSelectionStrategy() {
031: public boolean preselectAll() {
032: return true;
033: }
034:
035: public boolean preselectPackage() {
036: return true;
037: }
038:
039: public boolean preselectClass() {
040: return true;
041: }
042: };
043:
044: /**
045: * A strategy which preselects the invariants of the own package only.
046: */
047: public final static InvariantSelectionStrategy PRESELECT_PACKAGE = new InvariantSelectionStrategy() {
048: public boolean preselectAll() {
049: return false;
050: }
051:
052: public boolean preselectPackage() {
053: return true;
054: }
055:
056: public boolean preselectClass() {
057: return true;
058: }
059: };
060:
061: /**
062: * A strategy which preselects the invariants of the own class only.
063: */
064: public final static InvariantSelectionStrategy PRESELECT_CLASS = new InvariantSelectionStrategy() {
065: public boolean preselectAll() {
066: return false;
067: }
068:
069: public boolean preselectPackage() {
070: return false;
071: }
072:
073: public boolean preselectClass() {
074: return true;
075: }
076: };
077:
078: /**
079: * A strategy which preselects no invariants at all.
080: */
081: public final static InvariantSelectionStrategy PRESELECT_NONE = new InvariantSelectionStrategy() {
082: public boolean preselectAll() {
083: return false;
084: }
085:
086: public boolean preselectPackage() {
087: return false;
088: }
089:
090: public boolean preselectClass() {
091: return false;
092: }
093: };
094:
095: public abstract boolean preselectAll();
096:
097: public abstract boolean preselectPackage();
098:
099: public abstract boolean preselectClass();
100: }
|