Source Code Cross Referenced for InReachableStatePOBuilder.java in  » Testing » KeY » de » uka » ilkd » key » rule » metaconstruct » 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.metaconstruct 
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:        package de.uka.ilkd.key.rule.metaconstruct;
009:
010:        import de.uka.ilkd.key.java.JavaInfo;
011:        import de.uka.ilkd.key.java.Services;
012:        import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
013:        import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014:        import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
015:        import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
016:        import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
017:        import de.uka.ilkd.key.logic.*;
018:        import de.uka.ilkd.key.logic.op.*;
019:        import de.uka.ilkd.key.logic.sort.*;
020:        import de.uka.ilkd.key.rule.UpdateSimplifier;
021:        import de.uka.ilkd.key.rule.updatesimplifier.ArrayOfAssignmentPair;
022:        import de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair;
023:        import de.uka.ilkd.key.rule.updatesimplifier.Update;
024:        import de.uka.ilkd.key.rule.updatesimplifier.UpdateSimplifierTermFactory;
025:        import de.uka.ilkd.key.util.Debug;
026:
027:        /**
028:         * generates the proof obligation establishing that a given state describes
029:         * a legal pointer structure, i.e. that serveral system invariants are satisfied, like
030:         * no created object references a non-created one. 
031:         */
032:        public class InReachableStatePOBuilder extends TermBuilder {
033:
034:            private final UpdateFactory uf;
035:            private final Services services;
036:            private final Sort intSort;
037:            private final ProgramVariable created;
038:            private final Term TRUE;
039:            private final Term FALSE;
040:            private final ProgramVariable arraylength;
041:
042:            public InReachableStatePOBuilder(Services services) {
043:                uf = new UpdateFactory(services, new UpdateSimplifier());
044:                this .services = services;
045:                this .intSort = services.getTypeConverter().getIntegerLDT()
046:                        .targetSort();
047:                this .created = services.getJavaInfo().getAttribute(
048:                        ImplicitFieldAdder.IMPLICIT_CREATED,
049:                        services.getJavaInfo().getJavaLangObject());
050:                this .arraylength = services.getJavaInfo().getArrayLength();
051:                this .TRUE = TRUE(services);
052:                this .FALSE = FALSE(services);
053:            }
054:
055:            /**
056:             * Generates an optimized proof obligation, which is true if the state
057:             * described by update <tt>U</tt> in <tt>updateInReachableState:=U(<tt>inReachableState</tt>)</tt> 
058:             * leads to a legal pointer structure reachable from the current state.    
059:             */
060:            public Term generatePO(Term updateInReachableState) {
061:
062:                if (!(updateInReachableState.op() instanceof  IUpdateOperator)) {
063:                    return updateInReachableState;
064:                }
065:
066:                final IUpdateOperator updateOp = (IUpdateOperator) updateInReachableState
067:                        .op();
068:                if (updateOp instanceof  AnonymousUpdate) {
069:                    return updateInReachableState;
070:                }
071:                final Update update = Update
072:                        .createUpdate(updateInReachableState);
073:
074:                ListOfTerm conjunctions = SLListOfTerm.EMPTY_LIST;
075:                final ArrayOfAssignmentPair pairs = update
076:                        .getAllAssignmentPairs();
077:
078:                for (int i = 0; i < pairs.size(); i++) {
079:                    final AssignmentPair pair = pairs.getAssignmentPair(i);
080:                    final Location loc = pair.location();
081:
082:                    Term result = null;
083:                    if (loc instanceof  ProgramVariable
084:                            && loc.sort() != Sort.NULL) {
085:                        final ProgramVariable pv = (ProgramVariable) loc;
086:                        if (pv.isStatic()) {
087:                            if (pv.sort() instanceof  ObjectSort) {
088:                                result = staticFieldLiveRef(update, pair);
089:                            } else { // all implicit field are currently no reference fields
090:                                final ObjectSort containerType = (ObjectSort) pv
091:                                        .getContainerType().getSort();
092:                                ProgramVariable[] implicitFields = new ProgramVariable[] {
093:                                        cErroneous(containerType),
094:                                        cInitialized(containerType),
095:                                        cInInit(containerType),
096:                                        cPrepared(containerType),
097:                                        ntc(containerType) };
098:
099:                                if (pv == implicitFields[4]) {
100:                                    result = nextToCreateUpdatedSafely(update,
101:                                            pv);
102:                                } else {
103:                                    // if one of these fields is updated we need an additional axiom
104:                                    boolean additionalAxiom = true;
105:                                    if (pv == implicitFields[0]) {
106:                                        result = classErroneousUpdateIRSConform(
107:                                                update, implicitFields);
108:                                    } else if (pv == implicitFields[1]) {
109:                                        result = classInitializedUpdateIRSConform(
110:                                                update, implicitFields);
111:                                    } else if (pv == implicitFields[2]) {
112:                                        result = classInitInProgressUpdateIRSConform(
113:                                                update, implicitFields);
114:                                    } else {
115:                                        additionalAxiom = false;
116:                                    }
117:                                    if (additionalAxiom) {
118:                                        // in <tt>inReachableState</tt>, if a class is neither initialized, nor inInitialization, nor
119:                                        // erroneous (yes, objects of erroneous classes can exist) than no objects
120:                                        // are created
121:                                        final Term notErroneous = equals(
122:                                                var(implicitFields[0]), FALSE);
123:                                        final Term notInitialized = equals(
124:                                                var(implicitFields[1]), FALSE);
125:                                        final Term notInInit = equals(
126:                                                var(implicitFields[2]), FALSE);
127:                                        final Term ntcIsZero = equals(
128:                                                var(implicitFields[4]),
129:                                                zero(services));
130:                                        result = and(update(update, imp(and(
131:                                                and(notErroneous,
132:                                                        notInitialized),
133:                                                notInInit), ntcIsZero)), result);
134:                                    }
135:                                }
136:                            }
137:                        } else {
138:                            Debug.assertTrue(!pv.isMember());
139:                        }
140:                    } else if (loc instanceof  AttributeOp) {
141:                        final ProgramVariable pv = (ProgramVariable) ((AttributeOp) loc)
142:                                .attribute();
143:                        final Term refPrefix = ((AttributeOp) loc)
144:                                .referencePrefix(pair.locationAsTerm());
145:
146:                        if (refPrefix.sort() != Sort.NULL) {
147:                            if (loc.sort() instanceof  ObjectSort) {
148:                                final LogicVariable[] vPre = atPre(pair);
149:                                final Term[] tPre = var(vPre);
150:                                final Term preAx = preAx(tPre, pair
151:                                        .locationSubs());
152:                                result = update(update, imp(equals(dot(tPre[0],
153:                                        created), TRUE), createdOrNull(dot(
154:                                        tPre, (AttributeOp) loc))));
155:                                result = all(vPre, imp(preAx, result));
156:                            } else if (pv == created) {
157:                                if (refPrefix.op() instanceof  SortDependingFunction
158:                                        && ((SortDependingFunction) refPrefix
159:                                                .op())
160:                                                .getKind()
161:                                                .equals(
162:                                                        AbstractSort.OBJECT_REPOSITORY_NAME)) {
163:                                    result = createdInvariantForReposInstance(
164:                                            update, refPrefix);
165:                                } else {
166:                                    return updateInReachableState;
167:                                }
168:                            } else if (pv == arraylength) {
169:                                result = arrayLengthIsIRSConform(refPrefix,
170:                                        update);
171:                            }
172:                        }
173:                    } else if (loc instanceof  ArrayOp) {
174:                        final Sort elementSort = ((ArraySort) ((ArrayOp) loc)
175:                                .arraySort()).elementSort();
176:                        if (elementSort instanceof  ObjectSort) {
177:                            final LogicVariable[] vPre = atPre(pair);
178:                            final Term[] tPre = var(vPre);
179:                            final Term preAx = preAx(tPre, pair.locationSubs());
180:
181:                            // a@pre[i@pre]
182:                            final Term atPreArrayTerm = array((ArrayOp) loc,
183:                                    tPre);
184:
185:                            result = update(update, and(imp(equals(dot(tPre[0],
186:                                    created), TRUE),
187:                                    createdOrNull(atPreArrayTerm)),
188:                                    arrayStoreValid(tPre[0], atPreArrayTerm)));
189:
190:                            result = all(vPre, imp(preAx, result));
191:                        }
192:                    }
193:                    if (result != null) {
194:                        // take care of quantified updates    
195:                        result = quanUpdateClosure(pair, result);
196:
197:                        conjunctions = conjunctions.prepend(result);
198:                    }
199:                }
200:                conjunctions = conjunctions.prepend(globalInvariants(update));
201:                final Term po = conjunction(conjunctions.iterator());
202:
203:                // no free variables on top level
204:                Debug.assertTrue(po.freeVars().size() == 0);
205:
206:                return po;
207:            }
208:
209:            private Term arrayStoreValid(Term arrayRef, Term arrayValue) {
210:                final Function f = (Function) services.getNamespaces()
211:                        .functions().lookup(new Name("arrayStoreValid"));
212:                assert f != null : "ArrayStoreValid predicate not found.";
213:                return func(f, arrayRef, arrayValue);
214:            }
215:
216:            /**
217:             * in general an update of the <tt><created></tt> attribute would imply to show a large 
218:             * formula in order to ensure that the <tt>inReachableState</tt> property is preserved. In case of an update 
219:             * pair 
220:             *    <tt> T::<get>(idx).<created>=TRUE </tt>
221:             * the formula can be drastically reduced to  
222:             * <code>
223:             *    U( T::<get>(idx@pre).created = TRUE <-> 
224:             *         \exists int i; (i>=0               & 
225:             *                         i<T.<nextToCreate> & 
226:             *                         T::<get>(i) = T::<get>(idx@pre))    
227:             * </code>
228:             * (otherwise in case of <tt> o.<created>=TRUE </tt> one would need to 
229:             *  create the above formula for any subtype of <tt>o</t>'s static type)
230:             *  
231:             * This case is the most common case one usually gets. Other situations are rather artificially
232:             * and likely to be the result of faulty user interaction ;-)
233:             *  
234:             * @param update the Update to be checked
235:             * @param t_get the Term T::<get>(idx)
236:             * @return the relevant invariant 
237:             */
238:            private Term createdInvariantForReposInstance(Update update,
239:                    Term t_get) {
240:                Term result;
241:                final SortDependingFunction get = ((SortDependingFunction) t_get
242:                        .op());
243:                final ObjectSort os = (ObjectSort) get.getSortDependingOn();
244:                final LogicVariable lv = new LogicVariable(new Name("i"),
245:                        intSort);
246:
247:                final Term idx = t_get.sub(0);
248:                final LogicVariable idxPre = atPre(idx, 0);
249:                final Term t_idxPre = var(idxPre);
250:
251:                /*   pair = (T::<get>(idx).created:=b)
252:                          <code>
253:                              U( T::<get>(idx@pre).created = TRUE <-> 
254:                                 \exists int i; (i>=0               & 
255:                                                 i<T.<nextToCreate> & 
256:                                                 T::<get>(i) = T::<get>(idx@pre))    
257:                          </code>
258:                  
259:                 */
260:                final Term getPreIdx = func(get, t_idxPre);
261:
262:                result = equiv(equals(dot(getPreIdx, created), TRUE), ex(lv,
263:                        and(interval(zero(services), var(lv), var(ntc(os))),
264:                                equals(func(get, var(lv)), getPreIdx))));
265:
266:                return all(idxPre, imp(equals(idx, t_idxPre), update(update,
267:                        result)));
268:            }
269:
270:            /**
271:             * for each assignment pair of an update a formula is created with the relevant parts 
272:             * of the system invariants necessary to be shown to be preserved. This method computes
273:             * the closure of this formula wrt. quantified updates.  
274:             * 
275:             * @param pair the assignment pair used to determine the relevant parts of the
276:             * system invariant
277:             * @param relevantInvariants  the relevant part of the system invariants to be checked
278:             * for preserveness
279:             * @return the closure of the relvant invariant formula
280:             */
281:            private Term quanUpdateClosure(final AssignmentPair pair,
282:                    Term relevantInvariants) {
283:                Term closure = relevantInvariants;
284:                if (pair.nontrivialGuard()) {
285:                    closure = imp(pair.guard(), closure);
286:                }
287:                if (pair.boundVars().size() > 0) {
288:                    closure = tf.createQuantifierTerm(Op.ALL, pair.boundVars(),
289:                            closure);
290:                }
291:                return closure;
292:            }
293:
294:            /**
295:             * conjunction of terms that state global invariants, i.e. which have to be added to
296:             * the generated proof obligation in each case and where no optimisation is possible by
297:             * disregarding pieces by looking on the assignment pairs
298:             * @param update the Update to be checked to preserve <tt>inReachableState</tt>
299:             * @return global invariants
300:             */
301:            private Term globalInvariants(Update update) {
302:                return noObjectDeletion(update);
303:            }
304:
305:            /**
306:             * Generates a formula ensuring that an update (U) does not delete a former created
307:             * object. This created axiom is as follows:
308:             *     <code>
309:             *          \forall Object o; (o.<created> = TRUE -> U o.<created> = TRUE)
310:             *     </code> 
311:             * @param update the Update U which is checked for object deletion
312:             * @return a formula that evaluates to true if the update does not delete objects
313:             */
314:            private Term noObjectDeletion(Update update) {
315:                final LogicVariable o = new LogicVariable(new Name("o"),
316:                        services.getJavaInfo().getJavaLangObjectAsSort());
317:                final Term o_created = equals(dot(var(o), created), TRUE);
318:                return all(o, imp(o_created, update(update, o_created)));
319:            }
320:
321:            /**
322:             * Generates a formula checking that the given static field <tt>T.sv</tt> references <tt>null</tt>
323:             * or a created object.    
324:             * Let 
325:             *    <tt>pair=(T.sv := t)</tt>
326:             * the method assumes that loc is a static field of reference type ref (ref != Sort.NULL)
327:             * and generates the following formula
328:             * <code>
329:             *          U(T.<initialized>=TRUE -> T.sv.<created>=TRUE | T.sv = null)
330:             * </code>
331:             * ensuring that the static field is only updated to a living object or null
332:             * @param the update U to be checked
333:             * 
334:             * @return a formula that evaluates to true iff the update U does not update the
335:             * static field loc to an "illegal" value
336:             */
337:            private Term staticFieldLiveRef(Update update, AssignmentPair pair) {
338:                final ProgramVariable classInit = services.getJavaInfo()
339:                        .getAttribute(
340:                                ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
341:                                (((ProgramVariable) pair.location()))
342:                                        .getContainerType());
343:                return update(update, imp(equals(var(classInit), TRUE),
344:                        createdOrNull(pair.locationAsTerm())));
345:            }
346:
347:            /**
348:             * generates a formula that ensures that all ensuring that the updated 
349:             * field <tt>T.<nextToCreate></tt> still satisfies its invariants
350:             * namely that its value 
351:             *   <ul>
352:             *   <li>remains greater than or equals zero</li>
353:             *   <li>that all created objects have an index between 0 and T.<nextToCreate> </li>
354:             *   </ul>
355:             * <code>
356:             *   U ( T.<nextToCreate> >= 0 )  
357:             *     &
358:             *    -- unoptimized \forall int i; (i>=0 & i < T.<nextToCreate> <-> T::<get>(i).<created>=TRUE)         
359:             *    -- optimized
360:             *        \forall int i; (i>=T.<nextToCreate> & i < U(T.<nextToCreate>) -> U(T::<get>(i).<created>=TRUE))
361:             *     )   
362:             *   &
363:             *   T.<nextToCreate> <= U (T.<nextToCreate>)    
364:             * </code>
365:             * @param update the update to be checked
366:             * @param pv     the ProgramVariable representing <tt>T.<nextToCreate></tt>
367:             * @return a formula that evaluates to true if the update U does not destroy the 
368:             * system invariants of <tt>T.<nextToCreate></tt>
369:             */
370:            private Term nextToCreateUpdatedSafely(final Update update,
371:                    final ProgramVariable pv) {
372:                Term result;
373:                final ObjectSort os = (ObjectSort) pv.getContainerType()
374:                        .getSort();
375:                final LogicVariable iv = new LogicVariable(new Name("i"),
376:                        intSort);
377:
378:                final Term updatedPV = update(update, var(pv));
379:
380:                result = geq(updatedPV, zero(services), services);
381:
382:                final Term interval = interval(var(pv), var(iv), updatedPV);
383:
384:                result = and(result, all(iv, imp(interval, update(update,
385:                        equals(dot(func(rep(os), var(iv)), created),
386:                                TRUE(services))))));
387:
388:                result = and(result, leq(var(pv), updatedPV, services));
389:
390:                return result;
391:            }
392:
393:            /**
394:             * A class that is marked as erroneous is neither initialized nor is its initialization
395:             * in progress. 
396:             * 
397:             * If a class is marked erroneous its subclasses are not allowed to be initialized. It is
398:             * sufficient to test this property for its direct subclasses. As if 
399:             *    ...TODO
400:             * 
401:             * Additionally: from an <tt>inReachableState</tt> state with a class C marked erroneous, no state in 
402:             * <tt>inReachableState</tt> is reachable where the same class is not erroneous 
403:             * 
404:             * <code>
405:             *    U(C.<erroneous>   = TRUE -> (C.<classInitialized> = FALSE & 
406:             *                                 C.<initInProgress>   = FALSE)
407:             *    & 
408:             *    
409:             *    U(C.<erroneous>   = TRUE -> for all direct subtypes S of C: AND (S.<initialized> = FALSE) ) 
410:             *    
411:             *    &
412:             *    
413:             *    C.<erroneous>     = TRUE -> U(C.<erroneous> = TRUE)                      
414:             * </code>
415:             * @param update the Update describing the new state to be checked for the <tt>inReachableState</tt> property
416:             * @param erroneousField the ProgramVariable representing the static field <erroneous> of
417:             * a certain class type
418:             * @param implicitClassFields the ProgramVariables for the field 
419:             *    C.<erroneous>, C.<initialized>, C.<initInProgress> and C.<nextToCreate>
420:             *    (in this order)
421:             * @return a formula that evaluates to true if erroneous has been updated by U in an <tt>inReachableState</tt>
422:             * comforming way
423:             */
424:            private Term classErroneousUpdateIRSConform(Update update,
425:                    ProgramVariable[] implicitFields) {
426:
427:                final Term classErroneous = equals(var(implicitFields[0]), TRUE);
428:
429:                Term result = classFieldUpdateConform(update,
430:                        implicitFields[0], implicitFields[1],
431:                        implicitFields[2], null);
432:
433:                final KeYJavaType currentType = implicitFields[0]
434:                        .getContainerType();
435:                final ListOfKeYJavaType directSubTypes = getDirectSubtypes(currentType);
436:
437:                if (!directSubTypes.isEmpty()) {
438:                    final IteratorOfKeYJavaType it = directSubTypes.iterator();
439:                    Term subsNotInit = tt();
440:                    while (it.hasNext()) {
441:                        final ProgramVariable subsCInitPV = cInitialized((ObjectSort) it
442:                                .next().getSort());
443:                        subsNotInit = and(subsNotInit, equals(var(subsCInitPV),
444:                                FALSE));
445:                    }
446:                    result = and(result, update(update, subsNotInit));
447:                }
448:
449:                result = and(result, imp(classErroneous, update(update,
450:                        classErroneous)));
451:
452:                return result;
453:            }
454:
455:            /**
456:             * A class that is being initialized is neither initialized nor erroneous.   
457:             * <code>
458:             *    U(C.<initInProgress> = TRUE -> (C.<erroneous>        = FALSE & 
459:             *                                    C.<initialized>      = FALSE &
460:             *                                    C.<prepared>         = TRUE)        
461:             * </code>
462:             * @param update the Update describing the new state to be checked for the <tt>inReachableState</tt> property
463:             * @param erroneousField the ProgramVariable representing the static field <erroneous> of
464:             * a certain class type
465:             * @param implicitClassFields the ProgramVariables for the field 
466:             *    C.<erroneous>, C.<initialized>, C.<initInProgress> and C.<nextToCreate>
467:             *    (in this order)
468:             * @return a formula that evaluates to true if erroneous has been updated by U in an <tt>inReachableState</tt>
469:             * comforming way
470:             */
471:            private Term classInitInProgressUpdateIRSConform(Update update,
472:                    ProgramVariable[] implicitFields) {
473:
474:                Term result = classFieldUpdateConform(update,
475:                        implicitFields[2], implicitFields[0],
476:                        implicitFields[1], implicitFields[3]);
477:
478:                return result;
479:            }
480:
481:            /**
482:             * A class that is marked as initialized is neither initialized nor is its initialization
483:             * in progress. 
484:             * 
485:             * If a class is initialized all its supertypes must be initialized, too. It is sufficient
486:             * to look at the direct supertypes as if they are initialized all their supertypes are also
487:             * initialized in the prestate (as it has the <tt>inReachableState</tt> property) or their fields have been
488:             * updated and the formula ensuring this property for their supertypes will be 
489:             * (or have been) created when looking at the other assignment pairs of the update)
490:             * 
491:             * Additionally: from an <tt>inReachableState</tt> state with an initialized class C, no state in 
492:             * <tt>inReachableState</tt> is reachable where the same class is not initialized 
493:             * 
494:             * <code>
495:             *    U(C.<initialized> = TRUE -> (C.<erroneous>        = FALSE & 
496:             *                                 C.<initInProgress>   = FALSE & 
497:             *                                 C.<prepared>         = TRUE  )
498:             *    &
499:             *    
500:             *    U(C.<initialized> = TRUE -> for all direct supertypes S of C: AND (S.<initialized> = TRUE) ) 
501:             *    
502:             *    &
503:             *    C.<initialized>   = TRUE -> U(C.<initialized> = TRUE)                      
504:             * </code>
505:             * @param update the Update describing the new state to be checked for the <tt>inReachableState</tt> property
506:             * @param erroneousField the ProgramVariable representing the static field <erroneous> of
507:             * a certain class type
508:             * @param implicitClassFields the ProgramVariables for the field 
509:             *    C.<erroneous>, C.<initialized>, C.<initInProgress>, C.<prepared> and C.<nextToCreate>
510:             *    (in this order)
511:             * @return a formula that evaluates to true if erroneous has been updated by U in an <tt>inReachableState</tt>
512:             * comforming way
513:             */
514:            private Term classInitializedUpdateIRSConform(Update update,
515:                    ProgramVariable[] implicitFields) {
516:
517:                final Term classInitialized = equals(var(implicitFields[1]),
518:                        TRUE);
519:
520:                Term result = classFieldUpdateConform(update,
521:                        implicitFields[1], implicitFields[0],
522:                        implicitFields[2], implicitFields[3]);
523:                // direct supertypes
524:
525:                final ListOfKeYJavaType directSuperTypes = services
526:                        .getJavaInfo().getDirectSuperTypes(
527:                                implicitFields[0].getContainerType());
528:
529:                if (!directSuperTypes.isEmpty()) {
530:                    final IteratorOfKeYJavaType it = directSuperTypes
531:                            .iterator();
532:                    Term super TypesInit = tt();
533:                    while (it.hasNext()) {
534:                        final ProgramVariable super CInitPV = cInitialized((ObjectSort) it
535:                                .next().getSort());
536:                        super TypesInit = and(super TypesInit, equals(
537:                                var(super CInitPV), TRUE));
538:                    }
539:                    result = and(result, update(update, imp(classInitialized,
540:                            super TypesInit)));
541:                }
542:
543:                // reachable <tt>inReachableState</tt> state
544:                result = and(result, imp(classInitialized, update(update,
545:                        classInitialized)));
546:
547:                return result;
548:            }
549:
550:            /**
551:             * the length attribute of arrays is always creater or equal than zero
552:             * <code>
553:             *    \forall x; ((x = arrayReference & x!=null -> U(x.<created>=TRUE -> x.length >= 0)))
554:             * </code>
555:             */
556:            private Term arrayLengthIsIRSConform(Term arrayReference, Update u) {
557:                final LogicVariable preRef = atPre(arrayReference, 0);
558:                return all(preRef, imp(and(equals(var(preRef), arrayReference),
559:                        not(equals(var(preRef), NULL(services)))), update(u,
560:                        imp(equals(dot(var(preRef), created), TRUE(services)),
561:                                geq(dot(var(preRef), arraylength),
562:                                        zero(services), services)))));
563:            }
564:
565:            // helper method for class field pos
566:
567:            /**
568:             * @param currentType
569:             * @return
570:             */
571:            private ListOfKeYJavaType getDirectSubtypes(
572:                    final KeYJavaType currentType) {
573:                ListOfKeYJavaType directSubTypes = SLListOfKeYJavaType.EMPTY_LIST;
574:
575:                final JavaInfo javaInfo = services.getJavaInfo();
576:                final ListOfKeYJavaType allSubTypes = javaInfo
577:                        .getAllSubtypes(currentType);
578:
579:                final IteratorOfKeYJavaType subTypes = allSubTypes.iterator();
580:                while (subTypes.hasNext()) {
581:                    final KeYJavaType subtype = subTypes.next();
582:                    final ListOfKeYJavaType subsDirectSuper = javaInfo
583:                            .getDirectSuperTypes(subtype);
584:                    if (subsDirectSuper.contains(currentType)) {
585:                        directSubTypes = directSubTypes.prepend(subtype);
586:                    }
587:                }
588:                return directSubTypes;
589:            }
590:
591:            private Term classFieldUpdateConform(Update update,
592:                    ProgramVariable fieldA, ProgramVariable fieldB,
593:                    ProgramVariable fieldC, ProgramVariable fieldD) {
594:
595:                final Term classA = equals(var(fieldA), TRUE);
596:                final Term classNotB = equals(var(fieldB), FALSE);
597:                final Term classNotC = equals(var(fieldC), FALSE);
598:
599:                if (fieldD != null) {
600:                    return update(update, imp(classA, and(and(classNotB,
601:                            classNotC), equals(var(fieldD), TRUE))));
602:                }
603:
604:                return update(update, imp(classA, and(classNotB, classNotC)));
605:            }
606:
607:            // Helpers to build term    
608:            private Term conjunction(IteratorOfTerm it) {
609:                Term result = tt();
610:                while (it.hasNext()) {
611:                    result = and(result, it.next());
612:                }
613:                return result;
614:            }
615:
616:            private Term updateNoSimplification(Update update, Term target) {
617:                return UpdateSimplifierTermFactory.DEFAULT.createUpdateTerm(
618:                        update.getAllAssignmentPairs(), target);
619:            }
620:
621:            private Term update(Update update, Term target) {
622:                return uf.prepend(update, target);
623:            }
624:
625:            private Term createdOrNull(final Term t_o_a) {
626:                return or(equals(dot(t_o_a, created), TRUE), equals(t_o_a,
627:                        NULL(services)));
628:            }
629:
630:            private ProgramVariable ntc(ObjectSort os) {
631:                return services.getJavaInfo().getAttribute(
632:                        ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE, os);
633:            }
634:
635:            private ProgramVariable cInInit(ObjectSort os) {
636:                return services.getJavaInfo().getAttribute(
637:                        ImplicitFieldAdder.IMPLICIT_CLASS_INIT_IN_PROGRESS, os);
638:            }
639:
640:            private ProgramVariable cInitialized(ObjectSort os) {
641:                return services.getJavaInfo().getAttribute(
642:                        ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED, os);
643:            }
644:
645:            private ProgramVariable cPrepared(ObjectSort os) {
646:                return services.getJavaInfo().getAttribute(
647:                        ImplicitFieldAdder.IMPLICIT_CLASS_PREPARED, os);
648:            }
649:
650:            private ProgramVariable cErroneous(ObjectSort os) {
651:                return services.getJavaInfo().getAttribute(
652:                        ImplicitFieldAdder.IMPLICIT_CLASS_ERRONEOUS, os);
653:            }
654:
655:            private Term interval(Term lower, Term i, Term upper) {
656:                return and(geq(i, lower, services), lt(i, upper, services));
657:            }
658:
659:            private Function rep(ObjectSort os) {
660:                return (Function) ((SortDefiningSymbols) os)
661:                        .lookupSymbol(AbstractSort.OBJECT_REPOSITORY_NAME);
662:            }
663:
664:            /** creates an attribute term and takes care of shadowed attributes as well */
665:            private Term dot(Term[] subs, AttributeOp op) {
666:                return tf.createAttributeTerm(op, subs);
667:            }
668:
669:            /** creates an array term and takes care of shadowed attributes as well */
670:            private Term array(ArrayOp op, Term[] subs) {
671:                return tf.createArrayTerm(op, subs);
672:            }
673:
674:            private Term[] var(LogicVariable[] v) {
675:                final Term[] result = new Term[v.length];
676:                for (int i = 0; i < result.length; i++) {
677:                    result[i] = var(v[i]);
678:                }
679:                return result;
680:            }
681:
682:            private Term preAx(Term[] t1, Term[] t2) {
683:                Term result = tt();
684:                for (int i = 0; i < t1.length; i++) {
685:                    result = and(result, equals(t1[i], t2[i]));
686:                }
687:                return result;
688:            }
689:
690:            private LogicVariable atPre(Term t, int idx) {
691:                final Name name = new Name(t.sort().name().toString().charAt(0)
692:                        + "" + idx + "irs");
693:                return new LogicVariable(name, t.sort());
694:            }
695:
696:            private LogicVariable[] atPre(AssignmentPair pair) {
697:                final Term[] subs = pair.locationSubs();
698:                final LogicVariable[] result = new LogicVariable[subs.length];
699:                for (int i = 0; i < result.length; i++) {
700:                    result[i] = atPre(subs[i], i);
701:                }
702:                return result;
703:            }
704:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.