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.soundness;
012:
013: import org.apache.log4j.Logger;
014:
015: import de.uka.ilkd.key.gui.Main;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.logic.*;
018: import de.uka.ilkd.key.proof.Goal;
019: import de.uka.ilkd.key.proof.ListOfGoal;
020: import de.uka.ilkd.key.proof.TacletIndex;
021: import de.uka.ilkd.key.rule.*;
022:
023: /**
024: * This class is actually not used; taclet po are created through the methods of
025: * proof.init
026: */
027: public class TacletPORule implements BuiltInRule {
028:
029: private final Name name = new Name("Create Taclet PO");
030:
031: public TacletPORule() {
032: }
033:
034: /**
035: * returns true iff a rule is applicable at the given
036: * position. This does not necessary mean that a rule application
037: * will change the goal (this decision is made due to performance
038: * reasons)
039: */
040: public boolean isApplicable(Goal goal, PosInOccurrence pio,
041: Constraint userConstraint) {
042: if (pio == null) {
043: return true;
044: }
045: return false;
046: }
047:
048: public ListOfGoal apply(Goal goal, Services services,
049: RuleApp ruleApp) {
050: final Logger logger = Logger.getLogger("key.taclet_soundness");
051:
052: final TacletIndex tacletIndex = goal.ruleAppIndex()
053: .tacletIndex();
054:
055: POSelectionDialog dialog = new POSelectionDialog(Main
056: .getInstance().mediator(), tacletIndex
057: .allNoPosTacletApps());
058:
059: NoPosTacletApp app = dialog.getSelectedTaclets()[0];
060: //TODO: Extend for more than one taclet
061:
062: // TODO: well, we have to find a better way to cope with null
063:
064: logger.debug("Selected taclet: " + app);
065:
066: // StaticChecker sc = new StaticChecker ( services );
067: // sc.visit ( app.taclet (), false );
068:
069: POBuilder pob = new POBuilder(app, services);
070: pob.build();
071:
072: ListOfGoal newGoals = goal.split(1);
073:
074: newGoals.head().addFormula(
075: new ConstrainedFormula(pob.getPOTerm(),
076: Constraint.BOTTOM), false, false);
077:
078: updateNamespaces(newGoals.head(), pob);
079:
080: logger.debug("Resulting PO: " + app);
081:
082: return newGoals;
083: }
084:
085: private void updateNamespaces(Goal p_goal, POBuilder p_pob) {
086: NamespaceSet globalNss = p_goal.proof().getNamespaces();
087: Namespace funcNs = globalNss.functions();
088:
089: {
090: IteratorOfNamed it = p_pob.getFunctions().allElements()
091: .iterator();
092: while (it.hasNext())
093: funcNs.add(it.next());
094: }
095:
096: {
097: IteratorOfTacletApp it = p_pob.getTaclets().iterator();
098: TacletApp app;
099: while (it.hasNext()) {
100: app = it.next();
101: p_goal.addTaclet(app.taclet(), app.instantiations(),
102: app.constraint());
103: }
104: }
105: }
106:
107: public Name name() {
108: return name;
109: }
110:
111: public String displayName() {
112: return name().toString();
113: }
114:
115: public String toString() {
116: return name().toString();
117: }
118: }
|