Source Code Cross Referenced for TacletBuilder.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 java.util.HashMap;
014:
015:        import de.uka.ilkd.key.logic.*;
016:        import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
017:        import de.uka.ilkd.key.logic.op.QuantifiableVariable;
018:        import de.uka.ilkd.key.logic.op.SchemaVariable;
019:        import de.uka.ilkd.key.logic.sort.Sort;
020:
021:        /** subclasss build Schematic Theory Specific Rules (Taclets) */
022:        public abstract class TacletBuilder {
023:
024:            protected final static Name NONAME = new Name("unnamed");
025:
026:            protected Taclet taclet;
027:
028:            protected Name name = NONAME;
029:            protected Sequent ifseq = Sequent.EMPTY_SEQUENT;
030:            protected ListOfNewVarcond varsNew = SLListOfNewVarcond.EMPTY_LIST;
031:            protected ListOfNotFreeIn varsNotFreeIn = SLListOfNotFreeIn.EMPTY_LIST;
032:            protected ListOfNewDependingOn varsNewDependingOn = SLListOfNewDependingOn.EMPTY_LIST;
033:            protected ListOfTacletGoalTemplate goals = SLListOfTacletGoalTemplate.EMPTY_LIST;
034:            protected ListOfRuleSet ruleSets = SLListOfRuleSet.EMPTY_LIST;
035:            protected TacletAttributes attrs = new TacletAttributes();
036:            protected Constraint constraint = Constraint.BOTTOM;
037:            /** List of additional generic conditions on the instantiations of
038:             * schema variables. */
039:            protected ListOfVariableCondition variableConditions = SLListOfVariableCondition.EMPTY_LIST;
040:            protected HashMap goal2Choices = null;
041:            protected SetOfChoice choices = SetAsListOfChoice.EMPTY_SET;
042:
043:            private static boolean containsFreeVarSV(Term t) {
044:
045:                IteratorOfQuantifiableVariable it = t.freeVars().iterator();
046:                while (it.hasNext()) {
047:                    QuantifiableVariable var = it.next();
048:                    if (var instanceof  SchemaVariable
049:                            && ((SchemaVariable) var).isVariableSV()) {
050:                        return true;
051:                    }
052:                }
053:                return false;
054:            }
055:
056:            private static boolean containsFreeVarSV(Sequent s) {
057:                IteratorOfConstrainedFormula it = s.iterator();
058:                while (it.hasNext()) {
059:                    if (containsFreeVarSV(it.next().formula())) {
060:                        return true;
061:                    }
062:                }
063:                return false;
064:            }
065:
066:            static void checkContainsFreeVarSV(Sequent seq, Name tacletName,
067:                    String str) {
068:                if (containsFreeVarSV(seq)) {
069:                    throw new TacletBuilderException(tacletName,
070:                            "Free Variable in " + str
071:                                    + " in Taclet / sequent: " + seq);
072:                }
073:            }
074:
075:            static void checkContainsFreeVarSV(Term t, Name tacletName,
076:                    String str) {
077:                if (containsFreeVarSV(t)) {
078:                    throw new TacletBuilderException(tacletName,
079:                            "Free Variable found in " + str
080:                                    + " in Taclet / Term: " + t);
081:                }
082:            }
083:
084:            /** 
085:             * returns the name of the Taclet to be built
086:             */
087:            public Name getName() {
088:                return this .name;
089:            }
090:
091:            /** sets the name of the Taclet to be built
092:             */
093:            public void setName(Name name) {
094:                this .name = name;
095:            }
096:
097:            /** sets an optional display name (presented to the user)
098:             */
099:            public void setDisplayName(String s) {
100:                attrs.setDisplayName(s);
101:            }
102:
103:            /** adds an old name to the list of old names
104:             */
105:            public void addOldName(String s) {
106:                attrs.addOldName(s);
107:            }
108:
109:            public void setHelpText(String s) {
110:                attrs.setHelpText(s);
111:            }
112:
113:            /** sets the ifseq of the Taclet to be built
114:             */
115:            public void setIfSequent(Sequent seq) {
116:                checkContainsFreeVarSV(seq, getName(), "sequent");
117:                this .ifseq = seq;
118:            }
119:
120:            /** sets the constraint that has to be satisfied if the Taclet
121:             * should be valid */
122:            public void setConstraint(Constraint constraint) {
123:                this .constraint = constraint;
124:            }
125:
126:            /**
127:             * adds a mapping from GoalTemplate <code>gt</code> to SetOfChoice 
128:             * <code>soc</code>
129:             */
130:            public void addGoal2ChoicesMapping(TacletGoalTemplate gt,
131:                    SetOfChoice soc) {
132:                if (goal2Choices == null) {
133:                    goal2Choices = new HashMap();
134:                }
135:                goal2Choices.put(gt, soc);
136:            }
137:
138:            public HashMap getGoal2Choices() {
139:                return goal2Choices;
140:            }
141:
142:            public void setChoices(SetOfChoice choices) {
143:                this .choices = choices;
144:            }
145:
146:            public SetOfChoice getChoices() {
147:                return choices;
148:            }
149:
150:            /** adds a new <I>new</I> variable to the variable conditions of
151:             * the Taclet: v is new and has the sort as asSort if elementsort=false and the
152:             * sort of the elements of asSort if elementsort=true and asSort is a program
153:             * array SV. 
154:             */
155:            public void addVarsNew(SchemaVariable v, SchemaVariable asSort,
156:                    boolean elementsort) {
157:                addVarsNew(new NewVarcond(v, asSort, elementsort));
158:            }
159:
160:            /** adds a new <I>new</I> variable to the variable conditions of
161:             * the Taclet: v is new and has the sort as asSort
162:             */
163:            public void addVarsNew(SchemaVariable v, SchemaVariable asSort) {
164:                addVarsNew(new NewVarcond(v, asSort));
165:            }
166:
167:            /** adds a new <I>new</I> variable to the variable conditions of
168:             * the Taclet: v is new and has type sort
169:             */
170:            public void addVarsNew(SchemaVariable v, Sort sort) {
171:                addVarsNew(new NewVarcond(v, sort));
172:            }
173:
174:            /** adds a new <I>new</I> variable to the variable conditions of
175:             * the Taclet: v is new.
176:             */
177:            public void addVarsNew(NewVarcond nv) {
178:                if (!nv.getSchemaVariable().isProgramSV()) {
179:                    throw new TacletBuilderException(this ,
180:                            "Tried to add condition:" + nv
181:                                    + "to new vars-list. That can"
182:                                    + "match more than program" + " variables.");
183:                }
184:                varsNew = varsNew.prepend(nv);
185:            }
186:
187:            /** adds a list of <I>new</I> variables to the variable conditions of
188:             * the Taclet: v is new for all v's in the given list
189:             */
190:            public void addVarsNew(ListOfNewVarcond list) {
191:                IteratorOfNewVarcond it = list.iterator();
192:                while (it.hasNext()) {
193:                    addVarsNew(it.next());
194:                }
195:            }
196:
197:            /** adds a new <I>NotFreeIn</I> variable pair to the variable conditions of
198:             * the Taclet: v0 is not free in v1.
199:             */
200:            public void addVarsNotFreeIn(SchemaVariable v0, SchemaVariable v1) {
201:                varsNotFreeIn = varsNotFreeIn.prepend(new NotFreeIn(v0, v1));
202:            }
203:
204:            /** adds a list of <I>NotFreeIn</I> variable pairs to the variable 
205:             *conditions of
206:             * the Taclet: v0 is not free in v1 for all entries (v0,v1) in the given list.
207:             */
208:            public void addVarsNotFreeIn(ListOfNotFreeIn list) {
209:                varsNotFreeIn = varsNotFreeIn.prepend(list);
210:            }
211:
212:            /**
213:             * Add a "v0 depending on v1"-statement. "v0" may not occur within
214:             * the if sequent or the find formula/term, however, this is not
215:             * checked
216:             */
217:            public void addVarsNewDependingOn(SchemaVariable v0,
218:                    SchemaVariable v1) {
219:                varsNewDependingOn = varsNewDependingOn
220:                        .prepend(new NewDependingOn(v0, v1));
221:            }
222:
223:            /** Add an additional generic condition on the instatiation of
224:             * schema variables. */
225:            public void addVariableCondition(VariableCondition vc) {
226:                variableConditions = variableConditions.append(vc);
227:            }
228:
229:            /** adds a new goal descriptions to the goal descriptions of the Taclet.
230:             * The TacletGoalTemplate must be of 
231:             * the appropriate kind (Rewrite/Ante/Succ),
232:             * otherwise an IllegalArgumentException is thrown.
233:             */
234:            public abstract void addTacletGoalTemplate(TacletGoalTemplate goal);
235:
236:            /** adds a new rule set to the rule sets of the Taclet.
237:             */
238:            public void addRuleSet(RuleSet rs) {
239:                ruleSets = ruleSets.prepend(rs);
240:            }
241:
242:            public void setRuleSets(ListOfRuleSet rs) {
243:                ruleSets = rs;
244:            }
245:
246:            /** sets the noninteractive flag to the given value.
247:             */
248:            public void setNoninteractive(boolean ni) {
249:                attrs.setNoninteractive(ni);
250:            }
251:
252:            public Sequent ifSequent() {
253:                return ifseq;
254:            }
255:
256:            public ListOfTacletGoalTemplate goalTemplates() {
257:                return goals;
258:            }
259:
260:            public IteratorOfNotFreeIn varsNotFreeIn() {
261:                return varsNotFreeIn.iterator();
262:            }
263:
264:            public void setTacletGoalTemplates(ListOfTacletGoalTemplate g) {
265:                goals = g;
266:            }
267:
268:            /** builds and returns the Taclet that is specified by
269:             * former set... / add... methods. If no name is specified then
270:             * an Taclet with an empty string name is build. No specifications
271:             * for variable conditions, goals or rule sets imply that the
272:             * corresponding parts of the Taclet are empty. No specification for
273:             * the if-sequence is represented as a sequent with two empty
274:             * semisequences. No specification for the interactive or
275:             * recursive flags imply that the flags are not set. 
276:             * No specified find part for Taclets that require a find part
277:             * causes an IllegalStateException. 
278:             */
279:            public abstract Taclet getTaclet();
280:
281:            public Taclet getTacletWithoutInactiveGoalTemplates(
282:                    SetOfChoice active) {
283:                if (goal2Choices == null
284:                        || goals == SLListOfTacletGoalTemplate.EMPTY_LIST) {
285:                    return getTaclet();
286:                } else {
287:                    ListOfTacletGoalTemplate oldGoals = goals;
288:                    IteratorOfTacletGoalTemplate it = oldGoals.iterator();
289:                    Taclet result;
290:                    while (it.hasNext()) {
291:                        TacletGoalTemplate goal = it.next();
292:                        if (goal2Choices.get(goal) != null
293:                                && !((SetOfChoice) goal2Choices.get(goal))
294:                                        .subset(active)) {
295:                            goals = goals.removeAll(goal);
296:                        }
297:                    }
298:                    if (goals == SLListOfTacletGoalTemplate.EMPTY_LIST) {
299:                        result = null;
300:                    } else {
301:                        result = getTaclet();
302:                    }
303:                    goals = oldGoals;
304:                    return result;
305:                }
306:            }
307:
308:            static class TacletBuilderException extends
309:                    IllegalArgumentException {
310:
311:                private Name tacletname;
312:                private String errorMessage;
313:
314:                TacletBuilderException(Name tacletname, String errorMessage) {
315:                    this .tacletname = tacletname;
316:                    this .errorMessage = errorMessage;
317:                }
318:
319:                TacletBuilderException(TacletBuilder tb, String errorMessage) {
320:                    this (tb.getName(), errorMessage);
321:                }
322:
323:                public String getMessage() {
324:                    String message = (tacletname == null ? "(unknown taclet name)"
325:                            : tacletname.toString());
326:                    return message + ": " + errorMessage;
327:                }
328:
329:            }
330:
331:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.