Source Code Cross Referenced for GenericSortCondition.java in  » Testing » KeY » de » uka » ilkd » key » rule » inst » 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.inst 
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.inst;
012:
013:        import de.uka.ilkd.key.logic.op.SortDependingSymbol;
014:        import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
015:        import de.uka.ilkd.key.logic.sort.CollectionSort;
016:        import de.uka.ilkd.key.logic.sort.GenericSort;
017:        import de.uka.ilkd.key.logic.sort.Sort;
018:
019:        /**
020:         * Abstract superclass for conditions controlling the instantiations
021:         * of generic sorts
022:         */
023:        public abstract class GenericSortCondition {
024:
025:            private GenericSort gs;
026:
027:            /**
028:             * Create the condition that needs to be fulfilled for the given
029:             * instantiation of a metavariable to be correct, i.e. if the
030:             * schemavariable is of generic sort, the instantiation of that
031:             * sort has to match the sort of the schemavariable's
032:             * instantiation
033:             * @return the resulting condition, if the schemavariable is of
034:             * generic sort; null, if the sorts are either always compatible
035:             * (no generic sorts) or never compatible (non generic sorts that
036:             * don't match)
037:             */
038:            public static GenericSortCondition createCondition(
039:                    InstantiationEntry p_entry) {
040:
041:                if (!(p_entry instanceof  TermInstantiation))
042:                    return null;
043:
044:                final TermInstantiation ti = (TermInstantiation) p_entry;
045:                final SortedSchemaVariable ssv = (SortedSchemaVariable) p_entry
046:                        .getSchemaVariable();
047:
048:                return createCondition(ssv.sort(), ti.getTerm().sort(),
049:                        !subSortsAllowed(ssv));
050:            }
051:
052:            /**
053:             * Create a condition ensuring that the two given symbols become
054:             * identical; "p0" may be of generic sort, "p1" not
055:             * @return the resulting condition; null if the symbols are either
056:             * incompatible or equal
057:             */
058:            public static GenericSortCondition createCondition(
059:                    SortDependingSymbol p0, SortDependingSymbol p1) {
060:
061:                if (!p0.isSimilar(p1))
062:                    return null;
063:
064:                return createCondition(p0.getSortDependingOn(), p1
065:                        .getSortDependingOn(), true);
066:            }
067:
068:            /**
069:             * @return <code>true</code> iff the variable <code>p_sv</code> is
070:             *         allowed to be instantiated with expressions that have a real
071:             *         subtype of the type of <code>p_sv</code>. Otherwise the sorts
072:             *         have to match exactly
073:             */
074:            static boolean subSortsAllowed(SortedSchemaVariable p_sv) {
075:                return p_sv.isTermSV() && !p_sv.isStrict();
076:            }
077:
078:            /**
079:             * Create the condition to make a generic sort (s0) (or a
080:             * collection sort of a generic sort) and a concrete sort (s1)
081:             * equal
082:             * @param p_identity true iff an identity condition should be
083:             * generated (otherwise: a supersort condition is generated)
084:             * @return the resulting condition, if "s0" is of generic sort;
085:             * null, if the sorts are either always compatible (no generic
086:             * sorts) or never compatible (e.g. non generic sorts that don't
087:             * match)
088:             */
089:            protected static GenericSortCondition createCondition(Sort s0,
090:                    Sort s1, boolean p_identity) {
091:                while (s0 instanceof  CollectionSort) {
092:                    // Currently the sort hierarchy is not inherited by
093:                    // collection sorts; therefore identity has to be ensured
094:                    p_identity = true;
095:
096:                    if (!s0.getClass().equals(s1.getClass()))
097:                        return null;
098:
099:                    s0 = ((CollectionSort) s0).elementSort();
100:                    s1 = ((CollectionSort) s1).elementSort();
101:                }
102:
103:                if (!(s0 instanceof  GenericSort) || s1 == Sort.FORMULA)
104:                    return null;
105:
106:                final GenericSort gs = (GenericSort) s0;
107:
108:                if (p_identity) {
109:                    return createIdentityCondition(gs, s1);
110:                } else {
111:                    return createSupersortCondition(gs, s1);
112:                }
113:            }
114:
115:            /**
116:             * Create the condition to force the instantiation of a given
117:             * (possibly generic) sort
118:             * @param p_maximum hint whether the generic sort should be
119:             * instantiated with the maximum or mimimum possible concrete sort
120:             * (this hint is currently not used by GenericSortInstantiations)
121:             * @return the resulting condition, or null if "p_s" is not
122:             * generic
123:             */
124:            public static GenericSortCondition forceInstantiation(Sort p_s,
125:                    boolean p_maximum) {
126:
127:                if (p_s instanceof  GenericSort)
128:                    return createForceInstantiationCondition((GenericSort) p_s,
129:                            p_maximum);
130:                else if (p_s instanceof  CollectionSort)
131:                    return forceInstantiation(((CollectionSort) p_s)
132:                            .elementSort(), p_maximum);
133:
134:                return null;
135:            }
136:
137:            /**
138:             * @return a condition that specifies the given generic sort to be
139:             * instantiated with a supersort of the given concrete sort
140:             */
141:            public static GenericSortCondition createSupersortCondition(
142:                    GenericSort p_gs, Sort p_s) {
143:                return new GSCSupersort(p_gs, p_s);
144:            }
145:
146:            /**
147:             * @return a condition that specifies the given generic sort to be
148:             * instantiated (exactly) with the given concrete sort
149:             */
150:            public static GenericSortCondition createIdentityCondition(
151:                    GenericSort p_gs, Sort p_s) {
152:                return new GSCIdentity(p_gs, p_s);
153:            }
154:
155:            /**
156:             * @return a condition that specifies the given generic sort to be
157:             * instantiated
158:             * @param p_maximum hint whether the generic sort should be
159:             * instantiated with the maximum or mimimum possible concrete sort
160:             * (this hint is currently not used by GenericSortInstantiations)
161:             */
162:            public static GenericSortCondition createForceInstantiationCondition(
163:                    GenericSort p_gs, boolean p_maximum) {
164:                return new GSCForceInstantiation(p_gs, p_maximum);
165:            }
166:
167:            public GenericSort getGenericSort() {
168:                return gs;
169:            }
170:
171:            protected GenericSortCondition(GenericSort p_gs) {
172:                gs = p_gs;
173:            }
174:
175:            /** 
176:             * returns true if the given sort <code>s</code> satisfies this generic sort
177:             * condition
178:             * @param s the Sort to check 
179:             * @param insts a map containing already found instantiations
180:             * @return true if the given sort <code>s</code> satisfies this generic sort
181:             * condition
182:             */
183:            public abstract boolean check(Sort s,
184:                    GenericSortInstantiations insts);
185:
186:            static class GSCSupersort extends GenericSortCondition {
187:                Sort s;
188:
189:                protected GSCSupersort(GenericSort p_gs, Sort p_s) {
190:                    super (p_gs);
191:                    s = p_s;
192:                }
193:
194:                public Sort getSubsort() {
195:                    return s;
196:                }
197:
198:                /**
199:                 * checks if sort <code>p_s</code> is a supersort of 
200:                 * the <code>getSubsort</code>
201:                 */
202:                public boolean check(Sort p_s, GenericSortInstantiations insts) {
203:                    return getSubsort().extendsTrans(p_s);
204:                }
205:
206:                /** toString */
207:                public String toString() {
208:                    return "Supersort condition: " + getGenericSort() + " >= "
209:                            + getSubsort();
210:                }
211:
212:            }
213:
214:            static class GSCIdentity extends GenericSortCondition {
215:                Sort s;
216:
217:                protected GSCIdentity(GenericSort p_gs, Sort p_s) {
218:                    super (p_gs);
219:                    s = p_s;
220:                }
221:
222:                public Sort getSort() {
223:                    return s;
224:                }
225:
226:                /**
227:                 * tests if <code>p_s</code> is identical to @link GSCIdentity#getSort()        
228:                 */
229:                public boolean check(Sort p_s, GenericSortInstantiations insts) {
230:                    return p_s == getSort();
231:                }
232:
233:                /** toString */
234:                public String toString() {
235:                    return "Sort Identity: " + getGenericSort() + " = "
236:                            + getSort();
237:                }
238:            }
239:
240:            static class GSCForceInstantiation extends GenericSortCondition {
241:                boolean maximum;
242:
243:                protected GSCForceInstantiation(GenericSort p_gs,
244:                        boolean p_maximum) {
245:                    super (p_gs);
246:                    maximum = p_maximum;
247:                }
248:
249:                public boolean getMaximum() {
250:                    return maximum;
251:                }
252:
253:                /**
254:                 * checks if @link GenericSortcondition#getgenericSort()
255:                 * has been already instantiated by some sort
256:                 * (maximum, minimum is currently not checked)
257:                 */
258:                public boolean check(Sort p_s, GenericSortInstantiations insts) {
259:                    return insts.isInstantiated(getGenericSort());
260:                }
261:
262:                /** toString */
263:                public String toString() {
264:                    return "Force instantiation: " + getGenericSort() + ", "
265:                            + (getMaximum() ? "maximum" : "minimum");
266:                }
267:
268:            }
269:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.