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.encapsulation;
012:
013: import java.util.HashMap;
014: import java.util.Map;
015:
016: import de.uka.ilkd.key.java.ProgramElement;
017: import de.uka.ilkd.key.java.Services;
018: import de.uka.ilkd.key.logic.op.ArrayOfLocation;
019: import de.uka.ilkd.key.logic.op.IteratorOfProgramMethod;
020: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
021: import de.uka.ilkd.key.rule.inst.SVInstantiations;
022:
023: public class UniverseAnalyser {
024:
025: public static boolean showDialog = false;
026:
027: private void verbose(Object o) {
028: System.out.println(o);
029: }
030:
031: private void printStartup(ArrayOfLocation R, ArrayOfLocation P,
032: ArrayOfLocation F, ProgramElement pi) {
033: verbose("Universe analysis running with parameters...");
034: verbose("R = " + R);
035: verbose("P = " + P);
036: verbose("F = " + F);
037: verbose("pi = " + pi);
038: }
039:
040: private void printCoveredMethods(ListOfProgramMethod coveredMethods) {
041: verbose("The following method bodies have been analysed:");
042: IteratorOfProgramMethod it = coveredMethods.iterator();
043: int i = 1;
044: while (it.hasNext()) {
045: verbose("(" + i++ + ") " + it.next());
046: }
047: }
048:
049: private void printConstraints(
050: ListOfTypeSchemeConstraint constraints,
051: TypeSchemeConstraint andConstraint) {
052: verbose("The following constraints have been generated:");
053: IteratorOfTypeSchemeConstraint it = constraints.iterator();
054: int i = 1;
055: while (it.hasNext()) {
056: verbose("(" + i++ + ") " + it.next());
057: }
058:
059: verbose("The value ranges of the variables are:");
060: IteratorOfTypeSchemeVariable it2 = andConstraint.getFreeVars()
061: .iterator();
062: i = 1;
063: while (it2.hasNext()) {
064: TypeSchemeVariable var = it2.next();
065: verbose("(" + i++ + ") " + var + ": "
066: + var.getDefaultValue());
067: }
068: }
069:
070: private void printSolution(boolean success,
071: TypeSchemeConstraint andConstraint) {
072: if (success) {
073: verbose("A solution has been found:");
074:
075: IteratorOfTypeSchemeVariable it = andConstraint
076: .getFreeVars().iterator();
077: int i = 1;
078: while (it.hasNext()) {
079: TypeSchemeVariable var = it.next();
080: verbose("(" + i++ + ") " + var + ": " + var.evaluate());
081: }
082: } else {
083: verbose("No solution could be found.");
084: }
085: }
086:
087: public boolean analyse(ArrayOfLocation R, ArrayOfLocation P,
088: ArrayOfLocation F, ProgramElement pi,
089: SVInstantiations svInst, Services services) {
090: //give debug output
091: printStartup(R, P, F, pi);
092:
093: //check if pi contains any predefined local reference variables
094: //(not allowed)
095: FreeProgramVariableDetector fpvd = new FreeProgramVariableDetector(
096: pi);
097: if (fpvd.findFreePV()) {
098: verbose("There is a predefined local reference variable in pi. "
099: + "Canceling.");
100: return false;
101: }
102:
103: //create map for annotations
104: Map /*Location -> TypeSchemeTerm*/annotations = new HashMap();
105:
106: //annotate fields
107: for (int i = 0; i < R.size(); i++) {
108: annotations.put(R.getLocation(i), TypeSchemeUnion.REP);
109: }
110:
111: for (int i = 0; i < P.size(); i++) {
112: annotations.put(P.getLocation(i), TypeSchemeUnion.PEER);
113: }
114:
115: for (int i = 0; i < F.size(); i++) {
116: annotations.put(F.getLocation(i), TypeSchemeUnion.READONLY);
117: }
118:
119: //extract constraints
120: verbose("Generating constraints...");
121: TypeSchemeConstraintExtractor extractor = new TypeSchemeConstraintExtractor(
122: services);
123: ListOfTypeSchemeConstraint constraints = extractor.extract(pi,
124: annotations, svInst);
125: TypeSchemeConstraint andConstraint = new TypeSchemeAndConstraint(
126: constraints);
127:
128: //give debug output
129: printCoveredMethods(extractor.getCoveredMethods());
130: printConstraints(constraints, andConstraint);
131:
132: //try to solve the constraints
133: verbose("Trying to find a solution...");
134: TypeSchemeConstraintSolver solver = new TypeSchemeConstraintSolver();
135: boolean success = solver.solve(andConstraint);
136:
137: //give debug output
138: printSolution(success, andConstraint);
139:
140: //show dialog
141: if (!success && constraints.size() > 1 && showDialog) {
142: new UniverseDialog(constraints);
143: }
144:
145: //return result
146: verbose("Finished.");
147: return success;
148: }
149: }
|