Source Code Cross Referenced for Constraint.java in  » Testing » KeY » de » uka » ilkd » key » logic » 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.logic 
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.logic;
012:
013:        import de.uka.ilkd.key.java.Services;
014:        import de.uka.ilkd.key.logic.op.Metavariable;
015:        import de.uka.ilkd.key.logic.op.SetOfMetavariable;
016:
017:        /** Abstract constraint interface for constraints offering unification
018:         * of terms and joins. There are no public constructors to build up a
019:         * new Constraint use the BOTTOM constraint (static final class
020:         * variable) and add the needed constraints if a constraint would not
021:         * be satisfiable (cycles, unification failed) the Constraint TOP is
022:         * returned. TOP is as well as BOTTOM a static final class variable
023:         * (means usage of singleton pattern for Constraints BOTTOM and TOP).
024:         * Unsatisfiable constrains should only be representated by the TOP
025:         * element.
026:         */
027:
028:        public interface Constraint {
029:
030:            /** unsatisfiable Constraint */
031:            Constraint TOP = new Top();
032:            /** standard constraint class implementing the offered functionality */
033:            Constraint BOTTOM = new EqualityConstraint();
034:
035:            /** 
036:             * returns true if Bottom
037:             * @return true if Bottom 
038:             */
039:            boolean isBottom();
040:
041:            /**
042:             * a constraint being instance of this class is satisfiable. If a
043:             * method realizes that an unsatisfiable Constraint would be built
044:             * because of failed unification, cycle or s.th. similar it
045:             * returns the singleton TOP being instance of the subclass Top
046:             * @return true always 
047:             */
048:            boolean isSatisfiable();
049:
050:            /**
051:             * @return Find a term the given metavariable can be instantiated
052:             * with which is consistent with every instantiation that
053:             * satisfies this constraint (that means, the term such an
054:             * instantiation substitutes the metavariable with can always be
055:             * unified with the returned term).
056:             */
057:            Term getInstantiation(Metavariable p_mv);
058:
059:            /** 
060:             * tries to unify the terms t1 and t2
061:             * @param t1 Term to be unified 
062:             * @param t2 Term to be unified
063:             * @param services the Services providing access to the type model
064:             * the parameter may be <code>null</code> but then the 
065:             * unification fails (i.e. @link Constraint#TOP is returned) when accessing
066:             * the type model (e.g. for introducing intersection sorts) would be necessary). 
067:             *    
068:             * @return TOP if not possible, else a new constraint with after
069:             * unification of t1 and t2
070:             */
071:            Constraint unify(Term t1, Term t2, Services services);
072:
073:            /** 
074:             * tries to unify terms t1 and t2. 
075:             * @param t1 Term to be unfied 
076:             * @param t2 Term to be unfied
077:             * @param services the Services providing access to the type model
078:             * @param unchanged true iff the new constraint equals this one
079:             * @return TOP if not possible, else a new constraint with after
080:             * unification of t1 and t2
081:             */
082:            Constraint unify(Term t1, Term t2, Services services,
083:                    BooleanContainer unchanged);
084:
085:            /**
086:             * @return true iff this constraint is as strong as "co",
087:             * i.e. every instantiation satisfying "this" also satisfies "co".
088:             */
089:            boolean isAsStrongAs(Constraint co);
090:
091:            /**
092:             * @return true iff this constraint is as weak as "co",
093:             * i.e. every instantiation satisfying "co" also satisfies "this".
094:             */
095:            boolean isAsWeakAs(Constraint co);
096:
097:            /** checks equality of constraints
098:             */
099:            boolean equals(Object obj);
100:
101:            /** joins the given constraint with this constraint and returns
102:             * the joint new constraint.  Every implementing class should
103:             * handle the cases co == TOP and ( co instanceof EqualityConstraint ).
104:             * @param co Constraint to be joined with this one
105:             * @param services the Services providing access to the type model
106:             * @return the joined constraint 
107:             */
108:            Constraint join(Constraint co, Services services);
109:
110:            /** joins constraint co with this constraint and returns the joint
111:             * new constraint. The BooleanContainer is used to wrap a second
112:             * return value and indicates a subsumption of co by this
113:             * constraint. Every implementing class should handle the cases co
114:             * == TOP and ( co instanceof EqualityConstraint ).
115:             * @param co Constraint to be joined with this one
116:             * @param services the Services providing access to the type model
117:             * @param unchanged the BooleanContainers value set true, if this
118:             * constraint is as strong as co
119:             * @return the joined constraint     
120:             */
121:            Constraint join(Constraint co, Services services,
122:                    BooleanContainer unchanged);
123:
124:            /**
125:             * @return a constraint derived from this one by removing all
126:             * constraints on the given variable, which may therefore have any
127:             * value according to the new constraint (the possible values of
128:             * other variables are not modified)
129:             */
130:            Constraint removeVariables(SetOfMetavariable mvs);
131:
132:            /** @return String representation of the constraint */
133:            String toString();
134:
135:            /** Constraint class for representating the TOP (unsatisfiable) constraint. */
136:            class Top implements  Constraint {
137:
138:                /** creation of TOP */
139:                public Top() {
140:                }
141:
142:                /** is an unsatisfiable Constraint satisfiable? NO.
143:                 * @return always false
144:                 */
145:                public boolean isSatisfiable() {
146:                    return false;
147:                }
148:
149:                public Term getInstantiation(Metavariable p_mv) {
150:                    // As there is in fact no instantiation satisfying this
151:                    // constraint, we could return everything
152:                    return TermFactory.DEFAULT.createFunctionTerm(p_mv);
153:                }
154:
155:                /** adding new constraints to an unsatisfiable constraint
156:                 * results in an unsatisfiable constraint so this one is returned
157:                 * 
158:                 * @return always this
159:                 */
160:                public Constraint unify(Term t1, Term t2, Services services) {
161:                    return this ;
162:                }
163:
164:                public Constraint unify(Term t1, Term t2, Services services,
165:                        BooleanContainer unchanged) {
166:                    unchanged.setVal(true);
167:                    return this ;
168:                }
169:
170:                public boolean equals(Object obj) {
171:                    return (obj instanceof  Top);
172:                }
173:
174:                public boolean isAsStrongAs(Constraint co) {
175:                    // Nothing is stronger than this ...
176:                    return true;
177:                }
178:
179:                public boolean isAsWeakAs(Constraint co) {
180:                    // Nothing is stronger than this, except another Top
181:                    // instance
182:                    return (co instanceof  Top);
183:                }
184:
185:                /** joint of Top and co is Top
186:                 * @return this 
187:                 */
188:                public Constraint join(Constraint co, Services services) {
189:                    return this ;
190:                }
191:
192:                /** joint of Top and co is Top and Top subsumes every constraint
193:                 * @return this 
194:                 */
195:                public Constraint join(Constraint co, Services services,
196:                        BooleanContainer c) {
197:                    c.setVal(true);
198:                    return this ;
199:                }
200:
201:                /** returns true if Bottom
202:                 * @return true if Bottom 
203:                 */
204:                public boolean isBottom() {
205:                    return false;
206:                }
207:
208:                /**
209:                 * @return a constraint derived from this one by removing all
210:                 * constraints on the given variable, which may therefore have any
211:                 * value according to the new constraint (the possible values of
212:                 * other variables are not modified)
213:                 */
214:                public Constraint removeVariables(SetOfMetavariable mvs) {
215:                    // the constraint will still be unsatisfiable, as the
216:                    // other variables have no valid instantiations
217:                    return this ;
218:                }
219:
220:                /** @return String representing the TOP constraint 
221:                 */
222:                public String toString() {
223:                    return "TOP";
224:                }
225:
226:                public int hashCode() {
227:                    return 12345;
228:                }
229:            }
230:
231:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.