Source Code Cross Referenced for FindTaclet.java in  » Testing » KeY » de » uka » ilkd » key » rule » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.rule 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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;
012:
013:        import de.uka.ilkd.key.java.Services;
014:        import de.uka.ilkd.key.logic.*;
015:        import de.uka.ilkd.key.logic.op.*;
016:        import de.uka.ilkd.key.proof.Goal;
017:        import de.uka.ilkd.key.proof.IteratorOfGoal;
018:        import de.uka.ilkd.key.proof.ListOfGoal;
019:
020:        /** 
021:         * An abstract class to represent Taclets with a find part. This means, they
022:         * have to be attached to a formula or term of the sequent. This class is
023:         * extended by several subclasses to distinct between taclets that have to
024:         * attached to a top level formula of the antecedent ({@link AntecTaclet}),
025:         * to the succedent ({@link SuccTaclet}) or to an arbitrary term that matches
026:         * the find part somewhere in the sequent ({@link RewriteTaclet}).  
027:         */
028:        public abstract class FindTaclet extends Taclet {
029:
030:            /** contains the find term */
031:            protected Term find;
032:
033:            /** Set of schemavariables of the if and the (optional) find part */
034:            private SetOfSchemaVariable ifFindVariables = null;
035:
036:            /** this method is used to determine if top level updates are
037:             * allowed to be ignored. This is the case if we have an Antec or
038:             * SuccTaclet but not for a RewriteTaclet
039:             * @return true if top level updates shall be ignored 
040:             */
041:            protected abstract boolean ignoreTopLevelUpdates();
042:
043:            /** creates a FindTaclet 
044:             * @param name the Name of the taclet
045:             * @param applPart the TacletApplPart that contains the if-sequent, the
046:             * not-free and new-vars conditions 
047:             * @param goalTemplates a ListOfTacletGoalTemplate that contains all goaltemplates of
048:             * the taclet (these are the instructions used to create new goals when
049:             * applying the Taclet)
050:             * @param ruleSets a ListOfRuleSet that contains all rule sets the Taclet
051:             *      is attached to
052:             * @param constraint the Constraint of the Taclet (has to be fulfilled in
053:             * order to achieve this Taclet)
054:             * @param attrs the TacletAttributes encoding if the Taclet is non-interactive,
055:             * recursive or something like that
056:             * @param find the Term that is the pattern that has to be found in a
057:             * sequent and the places where it matches the Taclet can be applied
058:             * @param prefixMap a MapFromSchemaVariableToTacletPrefix that contains the
059:             * prefix for each SchemaVariable in the Taclet
060:             */
061:            public FindTaclet(Name name, TacletApplPart applPart,
062:                    ListOfTacletGoalTemplate goalTemplates,
063:                    ListOfRuleSet ruleSets, Constraint constraint,
064:                    TacletAttributes attrs, Term find,
065:                    MapFromSchemaVariableToTacletPrefix prefixMap,
066:                    SetOfChoice choices) {
067:                super (name, applPart, goalTemplates, ruleSets, constraint,
068:                        attrs, prefixMap, choices);
069:                this .find = find;
070:            }
071:
072:            /** returns the find term of the taclet to be matched */
073:            public Term find() {
074:                return find;
075:            }
076:
077:            /** 
078:             * matches the given term against the taclet's find term and
079:             * @param term the Term to be matched against the find expression 
080:             * of the taclet
081:             * @param matchCond the MatchConditions with side conditions to be 
082:             * satisfied, eg. partial instantiations of schema variables; before
083:             * calling this method the constraint contained in the match conditions
084:             * must be ensured to be satisfiable, i.e.
085:             *       <tt> matchCond.getConstraint ().isSatisfiable () </tt>
086:             * must return true
087:             * @param services the Services 
088:             * @param userConstraint a Constraint derived from user defined 
089:             * instantiations of meta variables
090:             * @return the found schema variable mapping or <tt>null</tt> if 
091:             * the matching failed
092:             */
093:            public MatchConditions matchFind(Term term,
094:                    MatchConditions matchCond, Services services,
095:                    Constraint userConstraint) {
096:                return match(term, find(), ignoreTopLevelUpdates(), matchCond,
097:                        services, userConstraint);
098:            }
099:
100:            /** CONSTRAINT NOT USED 
101:             * applies the replacewith part of Taclets
102:             * @param gt TacletGoalTemplate used to get the replaceexpression 
103:             * in the Taclet
104:             * @param goal the Goal where the rule is applied
105:             * @param posOfFind the PosInOccurrence belonging to the find expression
106:             * @param services the Services encapsulating all java information
107:             * @param matchCond the MatchConditions with all required instantiations 
108:             */
109:            protected abstract void applyReplacewith(TacletGoalTemplate gt,
110:                    Goal goal, PosInOccurrence posOfFind, Services services,
111:                    MatchConditions matchCond);
112:
113:            /**
114:             * adds the sequent of the add part of the Taclet to the goal sequent
115:             * @param add the Sequent to be added
116:             * @param goal the Goal to be updated
117:             * @param posOfFind the PosInOccurrence describes the place where to add
118:             * the semisequent 
119:             * @param services the Services encapsulating all java information
120:             * @param matchCond the MatchConditions with all required instantiations 
121:             */
122:            protected abstract void applyAdd(Sequent add, Goal goal,
123:                    PosInOccurrence posOfFind, Services services,
124:                    MatchConditions matchCond);
125:
126:            /**  
127:             * the rule is applied on the given goal using the
128:             * information of rule application. 
129:             * @param goal the goal that the rule application should refer to.
130:             * @param services the Services encapsulating all java information
131:             * @param ruleApp the taclet application that is executed.
132:             */
133:            public ListOfGoal apply(Goal goal, Services services,
134:                    RuleApp ruleApp) {
135:
136:                // Number without the if-goal eventually needed
137:                int numberOfNewGoals = goalTemplates().size();
138:
139:                TacletApp tacletApp = (TacletApp) ruleApp;
140:                MatchConditions mc = tacletApp.matchConditions();
141:
142:                // Restrict introduced metavariables to the subtree
143:                setRestrictedMetavariables(goal, mc);
144:
145:                ListOfGoal newGoals = checkIfGoals(goal, tacletApp
146:                        .ifFormulaInstantiations(), mc, numberOfNewGoals);
147:
148:                IteratorOfTacletGoalTemplate it = goalTemplates().iterator();
149:                IteratorOfGoal goalIt = newGoals.iterator();
150:
151:                while (it.hasNext()) {
152:                    TacletGoalTemplate gt = it.next();
153:                    Goal currentGoal = goalIt.next();
154:                    // add first because we want to use pos information that
155:                    // is lost applying replacewith
156:                    applyAdd(gt.sequent(), currentGoal, tacletApp
157:                            .posInOccurrence(), services, mc);
158:
159:                    applyReplacewith(gt, currentGoal, tacletApp
160:                            .posInOccurrence(), services, mc);
161:
162:                    applyAddrule(gt.rules(), currentGoal, services, mc);
163:
164:                    applyAddProgVars(gt.addedProgVars(), currentGoal, tacletApp
165:                            .posInOccurrence(), services, mc);
166:
167:                    currentGoal.setBranchLabel(gt.name());
168:                }
169:
170:                return newGoals;
171:            }
172:
173:            StringBuffer toStringFind(StringBuffer sb) {
174:                return sb.append("\\find(").append(find().toString()).append(
175:                        ")\n");
176:            }
177:
178:            /**
179:             * returns a representation of the Taclet with find part as String
180:             * @return string representation
181:             */
182:            public String toString() {
183:                if (tacletAsString == null) {
184:                    StringBuffer sb = new StringBuffer();
185:                    sb = sb.append(name()).append(" {\n");
186:                    sb = toStringIf(sb);
187:                    sb = toStringFind(sb);
188:                    sb = toStringVarCond(sb);
189:                    sb = toStringGoalTemplates(sb);
190:                    sb = toStringRuleSets(sb);
191:                    sb = toStringAttribs(sb);
192:                    tacletAsString = sb.append("}").toString();
193:                }
194:                return tacletAsString;
195:            }
196:
197:            /**
198:             * @return Set of schemavariables of the if and the (optional)
199:             * find part
200:             */
201:            public SetOfSchemaVariable getIfFindVariables() {
202:                if (ifFindVariables == null) {
203:                    TacletSchemaVariableCollector svc = new TacletSchemaVariableCollector();
204:                    find().execPostOrder(svc);
205:
206:                    ifFindVariables = getIfVariables();
207:                    IteratorOfSchemaVariable it = svc.varIterator();
208:                    while (it.hasNext())
209:                        ifFindVariables = ifFindVariables.add(it.next());
210:                }
211:
212:                return ifFindVariables;
213:            }
214:
215:            protected Taclet setName(String s, FindTacletBuilder b) {
216:                return super .setName(s, b);
217:            }
218:
219:            /**
220:             * Determine whether a replacewith-part is really supposed to modify
221:             * concerned formulas when applying a taclet (otherwise copies of the
222:             * formulas are created). Copies are created whenever the constraint of the
223:             * new formulas is stronger than the conjunction of the original
224:             * find-formula constraint and the user constraint. (Taking the user
225:             * constraint into account at this point ensures that the existence of the
226:             * user constraint is transparent to the user, and is a temporary solution
227:             * to cope with the absence of disunification constraints).
228:             * 
229:             * UPDATE: for the time being we are only considering the old constraint of
230:             * the formula (as the user constraint is more or less disable in
231:             * <code>TacletApp. canUseMVAPosteriori</code> right now)
232:             * 
233:             * @param goal
234:             *            the goal to which the taclet is applied
235:             * @param posOfFind
236:             *            position of the find-formula (which is the formula whose
237:             *            constraint is considered as the original formula constraint)
238:             * @param matchCond
239:             *            results of matching the taclet, in particular the new
240:             *            constraint that is attached to formulas added by replacewith
241:             * @return true iff replacewith is supposed to create copies of concerned
242:             *         formulas
243:             */
244:            protected boolean createCopies(Goal goal,
245:                    PosInOccurrence posOfFind, MatchConditions matchCond) {
246:                //        final Proof proof = goal.proof (); 
247:                //        final Constraint userConstraint =
248:                //            proof.getUserConstraint ().getConstraint ();
249:                final Constraint oriConstraint = posOfFind.constrainedFormula()
250:                        .constraint();
251:                //        final Constraint combinedConstraint =
252:                //            userConstraint.join ( oriConstraint, proof.getServices() );
253:                final Constraint newConstraint = matchCond.getConstraint();
254:                return !newConstraint.isAsWeakAs(oriConstraint);
255:            }
256:
257:            /** returns the variables in a Taclet with a read access
258:             */
259:            public ListOfSchemaVariable readSet() {
260:
261:                //List variables have to be collected to
262:                ListOfSchemaVariable readFromVarialbes = SLListOfSchemaVariable.EMPTY_LIST;
263:
264:                //List of Variables in find-part
265:                TacletSchemaVariableCollector tvarColl1 = new TacletSchemaVariableCollector() {
266:                    public void visit(Term t) {
267:                        if (t.op() instanceof  Modality
268:                                || t.op() instanceof  ModalOperatorSV) {
269:                            varList = collectSVInProgram(t.javaBlock(), varList);
270:                        }
271:                        for (int j = 0; j < t.arity(); j++) {
272:                            for (int i = 0; i < t.varsBoundHere(j).size(); i++) {
273:                                if (t.varsBoundHere(j).getQuantifiableVariable(
274:                                        i) instanceof  SchemaVariable) {
275:                                    varList = varList
276:                                            .prepend((SchemaVariable) t
277:                                                    .varsBoundHere(j)
278:                                                    .getQuantifiableVariable(i));
279:                                }
280:                            }
281:                        }
282:                    }
283:                };
284:                tvarColl1.visit(find());
285:
286:                //List of variables im add & replaceWith-Part
287:                TacletSchemaVariableCollector tvarColl2 = new TacletSchemaVariableCollector() {
288:                    public void visit(Term t) {
289:                        if (t.op() instanceof  SchemaVariable)
290:                            varList = varList.prepend((SchemaVariable) t.op());
291:                    }
292:                };
293:                tvarColl2.visitGoalTemplates(this , false);
294:
295:                // build intersection
296:                IteratorOfSchemaVariable it1 = tvarColl1.varIterator();
297:                while (it1.hasNext()) {
298:                    SchemaVariable sv1 = it1.next();
299:                    IteratorOfSchemaVariable it2 = tvarColl2.varIterator();
300:
301:                    while (it2.hasNext()) {
302:                        SchemaVariable sv2 = it2.next();
303:
304:                        if (sv1 == sv2) {
305:                            if (writeSet().head() != null) {
306:                                //if the variable belongs to the WriteSet, 
307:                                //remove it from the ReadSet
308:                                if (writeSet().head() != sv1)
309:                                    readFromVarialbes = readFromVarialbes
310:                                            .prepend(sv1);
311:                            } else
312:                                readFromVarialbes = readFromVarialbes
313:                                        .prepend(sv1);
314:                            break; //variable found, no need to keep searching
315:                        }
316:                    }
317:                }
318:                return readFromVarialbes;
319:            }
320:
321:            /** 
322:             * returns the variable in a Taclet to which is written to
323:             */
324:            public ListOfSchemaVariable writeSet() {
325:                IteratorOfTacletGoalTemplate it = goalTemplates().iterator();
326:                ListOfSchemaVariable updateVar = SLListOfSchemaVariable.EMPTY_LIST;
327:                Term replWith = null;
328:
329:                while (it.hasNext()) {
330:                    TacletGoalTemplate goalTemp = it.next();
331:
332:                    if (goalTemp instanceof  RewriteTacletGoalTemplate) {
333:                        replWith = ((RewriteTacletGoalTemplate) goalTemp)
334:                                .replaceWith();
335:
336:                        if (replWith.op() instanceof  IUpdateOperator) {
337:                            try {
338:                                updateVar = updateVar
339:                                        .prepend((SchemaVariable) replWith.sub(
340:                                                0).op());
341:                            } catch (ClassCastException e) {
342:                                System.err.println(name() + " "
343:                                        + replWith.sub(0).op().getClass());
344:                            }
345:                        }
346:                    }
347:                }
348:                return updateVar;
349:            }
350:
351:            /**
352:             * returns the variables that occur bound in the find part
353:             * @return the variables that occur bound in the find part
354:             */
355:            protected SetOfQuantifiableVariable getBoundVariablesHelper() {
356:                final BoundVarsVisitor bvv = new BoundVarsVisitor();
357:                bvv.visit(find());
358:                return bvv.getBoundVariables();
359:            }
360:
361:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.