Source Code Cross Referenced for ModifiesCheckProofOblInput.java in  » Testing » KeY » de » uka » ilkd » key » proof » init » 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.proof.init 
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:        package de.uka.ilkd.key.proof.init;
011:
012:        import java.util.*;
013:
014:        import recoder.io.PathList;
015:        import recoder.io.ProjectSettings;
016:
017:        import de.uka.ilkd.key.casetool.ModelMethod;
018:        import de.uka.ilkd.key.java.*;
019:        import de.uka.ilkd.key.java.abstraction.*;
020:        import de.uka.ilkd.key.java.declaration.ArrayDeclaration;
021:        import de.uka.ilkd.key.java.declaration.ClassDeclaration;
022:        import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
023:        import de.uka.ilkd.key.java.expression.literal.IntLiteral;
024:        import de.uka.ilkd.key.java.expression.operator.LessOrEquals;
025:        import de.uka.ilkd.key.java.expression.operator.LessThan;
026:        import de.uka.ilkd.key.java.expression.operator.New;
027:        import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
028:        import de.uka.ilkd.key.java.reference.ArrayReference;
029:        import de.uka.ilkd.key.java.reference.FieldReference;
030:        import de.uka.ilkd.key.java.reference.TypeRef;
031:        import de.uka.ilkd.key.java.reference.TypeReference;
032:        import de.uka.ilkd.key.java.statement.MethodBodyStatement;
033:        import de.uka.ilkd.key.java.visitor.ProgramTypeCollector;
034:        import de.uka.ilkd.key.jml.UsefulTools;
035:        import de.uka.ilkd.key.logic.*;
036:        import de.uka.ilkd.key.logic.op.*;
037:        import de.uka.ilkd.key.logic.sort.ObjectSort;
038:        import de.uka.ilkd.key.proof.ModifiesParserHelper;
039:        import de.uka.ilkd.key.proof.OpReplacer;
040:        import de.uka.ilkd.key.proof.Proof;
041:        import de.uka.ilkd.key.proof.ProofAggregate;
042:        import de.uka.ilkd.key.proof.RuleSource;
043:        import de.uka.ilkd.key.proof.mgt.Contract;
044:        import de.uka.ilkd.key.proof.mgt.Contractable;
045:        import de.uka.ilkd.key.util.Debug;
046:        import de.uka.ilkd.key.util.KeYExceptionHandler;
047:
048:        /** represents a proof obligation originating from a given Modifies Clause
049:         * as input for the prover.
050:         * @deprecated Replaced by RespectsModifiesPO.
051:         */
052:        public class ModifiesCheckProofOblInput implements  ProofOblInput {
053:
054:            private ModelMethod methRepr;
055:            protected String name;
056:
057:            protected InitConfig initConfig;
058:
059:            protected Term proofObl;
060:
061:            protected SetOfTerm modifiesElements;
062:            protected Set occuringClasses;
063:            protected Set currentClassAttributes;
064:
065:            protected KeYExceptionHandler exceptionHandler;
066:
067:            protected JavaInfo javaInfo;
068:            protected ProgramMethod m;
069:            protected String methodName;
070:
071:            protected ProgramVariable self;
072:            //private ProgramVariable pv;
073:            protected Vector pvVector;
074:
075:            protected HashMap location2descriptor = null;
076:
077:            //private Vector parameterNames = new Vector();
078:            protected Vector parameterTypes;
079:
080:            //    private Namespace ns = new Namespace();
081:
082:            private int resultNameCnt = 0;
083:
084:            /** the term factory used to create terms */
085:            final TermFactory tf = TermFactory.DEFAULT;
086:
087:            /** creates a new representation of a proof obligation from a Modifies 
088:             * Clause with the given name, originating from a representation of a model
089:             * method and having the given String as text of the Modifies Clause.
090:             * The given XMI file name can be used to read the underlying model.
091:             */
092:            public ModifiesCheckProofOblInput(String name, ModelMethod aMethRepr) {
093:                this .name = name
094:                        + (aMethRepr != null ? " " + aMethRepr.getName() : "");
095:                this .methRepr = aMethRepr;
096:            }
097:
098:            public String getJavaPath() {
099:                return methRepr.getContainingClass().getRootDirectory();
100:            }
101:
102:            /** returns false, that is the input never asks the user which
103:             * environment he prefers
104:             */
105:            public boolean askUserForEnvironment() {
106:                return false;
107:            }
108:
109:            public void setExceptionHandler(KeYExceptionHandler keh) {
110:                exceptionHandler = keh;
111:            }
112:
113:            /** generates the proof obligation
114:             *
115:             */
116:            public void readProblem(ModStrategy mod) {
117:                if (initConfig == null) {
118:                    throw new IllegalStateException("InitConfig not set.");
119:                }
120:
121:                javaInfo = initConfig.getServices().getJavaInfo();
122:
123:                getAllFromModParsHelper();
124:
125:                // extracts the signature as a list
126:                ListOfType signatureList = createSignatureList();
127:
128:                final KeYJavaType enclosingClassType = javaInfo
129:                        .getKeYJavaType(methRepr.getContainingClass()
130:                                .getFullClassName());
131:                // finds the current program method
132:                m = javaInfo.getProgramMethod(enclosingClassType, methodName,
133:                        signatureList, enclosingClassType);
134:                //last argument added. hope it is right. /AR
135:
136:                // puts all occuring classes into the set occuringClasses
137:                collectOccuringClasses(enclosingClassType);
138:
139:                this .proofObl = createProof();
140:            }
141:
142:            private void getAllFromModParsHelper() {
143:                ModifiesParserHelper modParserH = new ModifiesParserHelper(
144:                        methRepr, initConfig.getServices(), initConfig
145:                                .namespaces());
146:
147:                // starts the internal computation of the helper class
148:                modParserH.parseModifiesClauseToHashSet(methRepr
149:                        .getMyModifClause());
150:
151:                modifiesElements = modParserH.getModifiesElements();
152:                methodName = modParserH.getMethodName();
153:                self = modParserH.getPVSelf();
154:                pvVector = modParserH.getPVVector();
155:                parameterTypes = modParserH.getParameterTypesVector();
156:            }
157:
158:            private ListOfType createSignatureList() {
159:                ListOfType signatureList = SLListOfType.EMPTY_LIST;
160:                int index = parameterTypes.size() - 1;
161:                while (index >= 0) {
162:                    signatureList = signatureList.prepend((Type) parameterTypes
163:                            .elementAt(index));
164:                    index = index - 1;
165:                }
166:                return signatureList;
167:            }
168:
169:            protected void collectOccuringClasses(KeYJavaType type) {
170:                ProgramTypeCollector mCollector = new ProgramTypeCollector(m,
171:                        self, type, initConfig.getServices(), new HashSet());
172:                mCollector.start();
173:                occuringClasses = mCollector.getResult();
174:
175:                if (type != null) {
176:                    occuringClasses.add(type);
177:                }
178:
179:                // get the transitive closure of the occuring classes in the
180:                // sense that for each class the type of all its' attributes
181:                // is in the resulting Set
182:
183:                Set occuringClassesToAdd = (HashSet) ((HashSet) occuringClasses)
184:                        .clone();
185:                KeYJavaType current = null;
186:                while (!(occuringClassesToAdd.isEmpty())) {
187:                    current = (KeYJavaType) occuringClassesToAdd.iterator()
188:                            .next();
189:
190:                    Type currClassType = current.getJavaType();
191:                    KeYJavaType currentBase = current;
192:                    while (currClassType instanceof  ArrayDeclaration) {
193:                        currentBase = ((ArrayDeclaration) currClassType)
194:                                .getBaseType().getKeYJavaType();
195:                        currClassType = currentBase.getJavaType();
196:                    }
197:                    if (!(currClassType instanceof  PrimitiveType || currClassType instanceof  NullType)) {
198:                        // get all attributes of the given class
199:                        ListOfField allAttributes = javaInfo
200:                                .getKeYProgModelInfo()
201:                                .getAllFieldsLocallyDeclaredIn(currentBase);
202:
203:                        IteratorOfField iterateAttributes = allAttributes
204:                                .iterator();
205:
206:                        while (iterateAttributes.hasNext()) {
207:                            final ProgramVariable att = (ProgramVariable) iterateAttributes
208:                                    .next().getProgramVariable();
209:
210:                            if (!att.isImplicit()) {
211:                                final KeYJavaType addToOccCla = (KeYJavaType) att
212:                                        .getKeYJavaType();
213:                                if (!(occuringClasses.contains(addToOccCla))) {
214:                                    occuringClasses.add(addToOccCla);
215:                                    occuringClassesToAdd.add(addToOccCla);
216:                                }
217:                            }
218:                        }
219:                    }
220:                    occuringClassesToAdd.remove(current);
221:                }
222:            }
223:
224:            protected Term createProof() {
225:                Term formula;
226:                if (self != null) {
227:                    formula = tf.createJunctorTermAndSimplify(Op.IMP, tf
228:                            .createJunctorTerm(Op.NOT, tf.createEqualityTerm(tf
229:                                    .createVariableTerm(self), tf
230:                                    .createFunctionTerm(Op.NULL))),
231:                            createProofStart());
232:                } else {
233:                    formula = createProofStart();
234:                }
235:                return formula;
236:            }
237:
238:            protected Term createProofStart() {
239:                Iterator iterateClasses = occuringClasses.iterator();
240:                Term accumulateClassFormulas = tf.createJunctorTerm(Op.TRUE);
241:                KeYJavaType currClass;
242:                while (iterateClasses.hasNext()) {
243:                    currClass = (KeYJavaType) iterateClasses.next();
244:                    if (javaInfo.getNullType() != currClass) {
245:                        accumulateClassFormulas = tf
246:                                .createJunctorTermAndSimplify(Op.AND,
247:                                        createClassFormula(currClass),
248:                                        accumulateClassFormulas);
249:                    }
250:                }
251:                return tf.createJunctorTermAndSimplify(Op.IMP, tf
252:                        .createFunctionTerm(javaInfo.getInReachableState()),
253:                        accumulateClassFormulas);
254:            }
255:
256:            private Term createClassFormula(KeYJavaType currClass) {
257:                LogicVariable oprime = new LogicVariable(new Name("o"),
258:                        currClass.getSort());
259:
260:                // generate formula starting with \forall o': currClass
261:                Term classFormula = tf.createQuantifierTerm(Op.ALL, oprime,
262:                        createClassSubFormula(currClass, oprime));
263:
264:                return classFormula;
265:            }
266:
267:            private Term createClassSubFormula(KeYJavaType currClass,
268:                    LogicVariable oprime) {
269:                Type currClassType = currClass.getJavaType();
270:                // stop primitive types from getting checked for attributes, there are
271:                // none anyway
272:                if (currClassType instanceof  PrimitiveType) {
273:                    return tf.createJunctorTerm(Op.TRUE);
274:                }
275:
276:                Term classSubFormula;
277:
278:                ListOfField allAttributes;
279:                // get all attributes of the given class
280:                if (currClassType instanceof  ClassDeclaration) {
281:                    allAttributes = javaInfo.getKeYProgModelInfo()
282:                            .getAllFieldsLocallyDeclaredIn(
283:                                    javaInfo.getKeYJavaType(currClassType));
284:                    IteratorOfField iterateAttributes = allAttributes
285:                            .iterator();
286:
287:                    // initial value is TRUE which is the value of an empty conjunction
288:                    // as this formula is a conjunction this is the correct value in 
289:                    // case there are no elements
290:                    Term accumulateAttributeFormulas = tf
291:                            .createJunctorTerm(Op.TRUE);
292:
293:                    ProgramVariable currAttribute = null;
294:
295:                    while (iterateAttributes.hasNext()) {
296:                        currAttribute = (ProgramVariable) iterateAttributes
297:                                .next().getProgramVariable();
298:
299:                        accumulateAttributeFormulas = tf
300:                                .createJunctorTermAndSimplify(Op.AND,
301:                                        createAttributeFormula(currAttribute,
302:                                                currClass, oprime),
303:                                        accumulateAttributeFormulas);
304:                    }
305:
306:                    classSubFormula = accumulateAttributeFormulas;
307:
308:                } else {
309:                    // maybe check whether it is an ArrayDeclaration with test below:
310:                    // check it; may be artificial nulltype
311:                    if (currClassType instanceof  ArrayDeclaration) {
312:                        classSubFormula = createArrayFormula(currClass, oprime);
313:                    } else {
314:                        // is this correct?
315:                        classSubFormula = tf.createJunctorTerm(Op.TRUE);
316:                    }
317:                }
318:
319:                Term nullTerm = tf.createFunctionTerm(Op.NULL);
320:                Term ov = tf.createVariableTerm(oprime);
321:                Term nn = tf.createJunctorTerm(Op.NOT, tf.createEqualityTerm(
322:                        ov, nullTerm));
323:
324:                Term eqc = UsefulTools.isCreated(ov, initConfig.getServices());
325:                ProgramVariable ci = initConfig.getServices().getJavaInfo()
326:                        .getAttribute(
327:                                ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
328:                                (ObjectSort) oprime.sort());
329:
330:                Term eqi = tf.createEqualityTerm(tf.createVariableTerm(ci),
331:                        initConfig.getServices().getTypeConverter()
332:                                .convertToLogicElement(BooleanLiteral.TRUE));
333:                eqc = tf.createJunctorTermAndSimplify(Op.AND, eqc, eqi);
334:                classSubFormula = tf.createJunctorTermAndSimplify(Op.IMP, tf
335:                        .createJunctorTerm(Op.AND, nn, eqc), classSubFormula);
336:                return classSubFormula;
337:            }
338:
339:            private Term createAttributeFormula(ProgramVariable currAttribute,
340:                    KeYJavaType currClass, LogicVariable oprime) {
341:                if (!currAttribute.isImplicit()) {
342:
343:                    // create conjunction of o' != o111, o' != o112, ... for non-static
344:                    // create "false" in case of a static attribute which is part of
345:                    // the modifies clause and "true" if it not part of the m.c.
346:
347:                    // some initial value
348:                    Term ante = tf.createJunctorTerm(Op.TRUE);
349:
350:                    IteratorOfTerm modifiesIterator = modifiesElements
351:                            .iterator();
352:                    TypeConverter typeConv = initConfig.getServices()
353:                            .getTypeConverter();
354:                    final Term t_oprime = tf.createVariableTerm(oprime);
355:
356:                    while (modifiesIterator.hasNext()) {
357:                        Term modTerm = modifiesIterator.next();
358:
359:                        if ((!(modTerm.op() instanceof  ProgramVariable) || ((ProgramVariable) modTerm
360:                                .op()).isStatic())
361:                                && !(modTerm.op() instanceof  ArrayOp)) {
362:                            ante = createModifiesFormulaForAttribute(
363:                                    currAttribute, currClass, ante, modTerm,
364:                                    typeConv, t_oprime);
365:                        } else {
366:                            if (modTerm.op() instanceof  ProgramVariable) {
367:                                // The modifies element has been a single ProgramVariable,
368:                                // meaning no dereferencing has happened. In this case there
369:                                // is nothing that can be done because this shouldn't happen
370:                                // Only attributes can be changed and thus only those are 
371:                                // relevant in the modifies clause.
372:                                // THROW EXCEPTION HERE !!!
373:                                System.out
374:                                        .println("Error - Element with no dereferencing "
375:                                                + "in the modifies clause: "
376:                                                + modTerm);
377:                            }
378:                            if (modTerm.op() instanceof  ArrayOp) {
379:                                // nothing to do here as an array element is not
380:                                // relevant for a normal attribute
381:                            }
382:                        }
383:                    }
384:
385:                    // create part after the implication arrow
386:                    LogicVariable x = new LogicVariable(new Name("x"),
387:                            currAttribute.getKeYJavaType().getSort());
388:
389:                    // Create the MethodReference belonging to the method whose modifies
390:                    // clause is being checked here.
391:                    Expression[] p = new Expression[pvVector.size()];
392:                    for (int i = 0; i < pvVector.size(); i = i + 1) {
393:                        p[i] = (ProgramVariable) pvVector.elementAt(i);
394:                    }
395:
396:                    StatementBlock mBlock = createMethodCall(p);
397:
398:                    final Term t_x = tf.createVariableTerm(x);
399:                    final Term primedAttribute = tf.createAttributeTerm(
400:                            currAttribute, t_oprime);
401:
402:                    Term post = tf.createQuantifierTerm(Op.ALL, x, tf
403:                            .createJunctorTermAndSimplify(Op.IMP, tf
404:                                    .createEqualityTerm(t_x, primedAttribute),
405:                                    tf.createBoxTerm(JavaBlock
406:                                            .createJavaBlock(mBlock), tf
407:                                            .createEqualityTerm(t_x,
408:                                                    primedAttribute))));
409:
410:                    return tf.createJunctorTermAndSimplify(Op.IMP, ante, post);
411:                } else {
412:                    return tf.createJunctorTerm(Op.TRUE);
413:                }
414:            }
415:
416:            /**
417:             * @param currAttribute
418:             * @param currClass
419:             * @param ante
420:             * @param modProgVar
421:             * @param typeConv
422:             * @param t_oprime
423:             * @return
424:             */
425:            private Term createModifiesFormulaForAttribute(
426:                    ProgramVariable currAttribute, KeYJavaType currClass,
427:                    Term ante, Term modTerm, TypeConverter typeConv,
428:                    final Term t_oprime) {
429:
430:                // static attribute
431:                if (modTerm.op() instanceof  ProgramVariable) {
432:                    // Check if the attributes match
433:                    if (modTerm.op() == currAttribute) {
434:                        // build formula
435:                        ante = tf.createJunctorTerm(Op.FALSE);
436:                    }
437:                } else {
438:                    ProgramVariable modProgAttrib = (ProgramVariable) ((AttributeOp) modTerm
439:                            .op()).attribute();
440:                    BasicLocationDescriptor bloc = (BasicLocationDescriptor) location2descriptor
441:                            .get(modTerm);
442:                    modTerm = modTerm.sub(0);
443:
444:                    KeYJavaType classType = javaInfo.getKeYJavaType(modTerm
445:                            .sort());
446:                    // Check if the Class Types match
447:                    if (classType == currClass) {
448:                        // Check if the attributes match
449:                        if (modProgAttrib == currAttribute) {
450:                            Term anteSub = tf.createJunctorTerm(Op.NOT, tf
451:                                    .createEqualityTerm(t_oprime, modTerm));
452:                            anteSub = tf.createJunctorTermAndSimplify(Op.IMP,
453:                                    bloc.getFormula(), anteSub);
454:                            // quantify free variables in the prefix
455:                            if (modTerm.freeVars().size() > 0) {
456:                                anteSub = tf
457:                                        .createQuantifierTerm(
458:                                                Op.ALL,
459:                                                new ArrayOfQuantifiableVariable(
460:                                                        modTerm.freeVars()
461:                                                                .toArray()),
462:                                                anteSub);
463:                            }
464:                            // build formula
465:                            ante = tf.createJunctorTermAndSimplify(Op.AND,
466:                                    anteSub, ante);
467:                        }
468:                    }
469:                }
470:                return ante;
471:
472:            }
473:
474:            private Term createArrayFormula(KeYJavaType currClass,
475:                    LogicVariable oprime) {
476:                // create conjunction of o' != o111, o' != o112, ... 
477:                // all this with a "check" before it for the right array index
478:
479:                TypeConverter typeConv = initConfig.getServices()
480:                        .getTypeConverter();
481:
482:                LogicVariable lambda = new LogicVariable(new Name("lambda"),
483:                        typeConv.getIntegerLDT().targetSort());
484:
485:                // initial value true, as it is the value of an empty conjunction
486:                // and our terms are connected conjunctively	
487:                Term ante = tf.createJunctorTerm(Op.TRUE);
488:
489:                IteratorOfTerm modifiesIterator = modifiesElements.iterator();
490:                while (modifiesIterator.hasNext()) {
491:                    Term modTerm = modifiesIterator.next();
492:                    //	    modElm = typeConv.convertToProgramElement(modTerm);
493:
494:                    //	    modProgVar = modElm;
495:
496:                    //check whether it is appropriate to add this to the ante
497:                    //	    if (modProgVar instanceof ArrayReference){
498:                    if (modTerm.op() instanceof  ArrayOp
499:                            && javaInfo.getKeYJavaType(modTerm.sub(0).sort()) == currClass) {
500:                        Term preCond = tf.createJunctorTerm(Op.TRUE);
501:                        if (modTerm.sub(1).freeVars().size() == 0) {
502:                            preCond = tf.createEqualityTerm(modTerm.sub(1), tf
503:                                    .createVariableTerm(lambda));
504:                        }
505:                        Debug.assertTrue(modTerm.sub(1).freeVars().size() <= 1);
506:                        BasicLocationDescriptor bloc = (BasicLocationDescriptor) location2descriptor
507:                                .get(modTerm);
508:                        HashMap replaceMap = new HashMap();
509:                        replaceMap.put(modTerm.sub(1).freeVars().iterator()
510:                                .next(), lambda);
511:                        OpReplacer or = new OpReplacer(replaceMap);
512:                        preCond = tf.createJunctorTermAndSimplify(Op.AND,
513:                                preCond, or.replace(bloc.getFormula()));
514:                        // o' != o_ij
515:                        Term postCond = tf.createJunctorTerm(Op.NOT, tf
516:                                .createEqualityTerm(tf
517:                                        .createVariableTerm(oprime), modTerm
518:                                        .sub(0)));
519:
520:                        Term cond = tf.createJunctorTermAndSimplify(Op.IMP,
521:                                preCond, postCond);
522:
523:                        // quantify free variables in the prefix
524:                        if (modTerm.sub(0).freeVars().size() > 0) {
525:                            cond = tf
526:                                    .createQuantifierTerm(Op.ALL,
527:                                            new ArrayOfQuantifiableVariable(
528:                                                    modTerm.sub(0).freeVars()
529:                                                            .toArray()), cond);
530:                        }
531:
532:                        // build parts together into the ante formula
533:                        ante = tf.createJunctorTermAndSimplify(Op.AND, cond,
534:                                ante);
535:                    } else {
536:                        // The modifies element has not been an ArrayReference,
537:                        // that means it has nothing to do with the current class/array
538:                        // as that is an array and we can thus ignore this element of
539:                        // the modifies clause
540:                    }
541:                }
542:
543:                // create part after the outer implication arrow
544:                LogicVariable x = new LogicVariable(new Name("x"),
545:                        ((ArrayDeclaration) currClass.getJavaType())
546:                                .getBaseType().getKeYJavaType().getSort());
547:
548:                // Create the MethodReference belonging to the method whose modifies
549:                // clause is being checked here.
550:                Expression[] p = new Expression[pvVector.size()];
551:                for (int i = 0; i < pvVector.size(); i = i + 1) {
552:                    p[i] = (ProgramVariable) pvVector.elementAt(i);
553:                }
554:
555:                StatementBlock mBlock = createMethodCall(p);
556:
557:                Term equality = tf.createEqualityTerm(tf.createVariableTerm(x),
558:                        tf.createArrayTerm(ArrayOp.getArrayOp(oprime.sort()),
559:                                tf.createVariableTerm(oprime), tf
560:                                        .createVariableTerm(lambda)));
561:
562:                Term post = tf.createQuantifierTerm(Op.ALL, x, tf
563:                        .createJunctorTermAndSimplify(Op.IMP, equality, tf
564:                                .createBoxTerm(JavaBlock
565:                                        .createJavaBlock(mBlock), equality)));
566:
567:                Term arrayFormula = tf.createJunctorTermAndSimplify(Op.IMP,
568:                        ante, post);
569:
570:                // helpers for the next block below
571:                final Function leq = typeConv.getIntegerLDT().getLessOrEquals();
572:                final Function lt = typeConv.getIntegerLDT().getLessThan();
573:                final Term zero = typeConv.getIntegerLDT().translateLiteral(
574:                        new IntLiteral(0));
575:                final Term validArrayTerm0 = tf.createFunctionTerm(leq, zero,
576:                        tf.createVariableTerm(lambda));
577:                final ProgramVariable lengthPV = (ProgramVariable) ((ArrayDeclaration) currClass
578:                        .getJavaType()).length().getFieldSpecifications()
579:                        .getFieldSpecification(0).getProgramVariable();
580:                final Term lengthTerm = tf.createAttributeTerm(lengthPV, tf
581:                        .createVariableTerm(oprime));
582:                final Term validArrayTerm1 = tf.createFunctionTerm(lt, tf
583:                        .createVariableTerm(lambda), lengthTerm);
584:
585:                // creates the 0<= lambda /\ lambda < o'.length() -> rest
586:                arrayFormula = tf.createJunctorTermAndSimplify(Op.IMP, tf
587:                        .createJunctorTermAndSimplify(Op.AND, validArrayTerm0,
588:                                validArrayTerm1), arrayFormula);
589:
590:                // generate and return formula starting with \forall \lambda: int
591:                return tf.createQuantifierTerm(Op.ALL, lambda, arrayFormula);
592:            }
593:
594:            private StatementBlock createMethodCall(Expression[] p) {
595:                if (m.isConstructor()) {
596:                    TypeRef prefix = new TypeRef(self.getKeYJavaType());
597:                    New n = new New(p, prefix, prefix);
598:                    return new StatementBlock(n);
599:                } else {
600:                    ProgramVariable result = null;
601:                    if (m.getKeYJavaType() != null) {
602:                        result = new LocationVariable(new ProgramElementName(
603:                                "_result" + resultNameCnt++), m
604:                                .getKeYJavaType());
605:                        initConfig.namespaces().programVariables().add(result);
606:                    }
607:                    MethodBodyStatement mBS = new MethodBodyStatement(m, self,
608:                            result, new ArrayOfExpression(p));
609:                    return new StatementBlock(mBS);
610:                }
611:            }
612:
613:            public ProofAggregate getPO() {
614:                if (proofObl == null)
615:                    throw new IllegalStateException("No proofObl term");
616:                // now a static call since there is no suitable common superclass
617:                String s = OCLProofOblInput.createProofHeader(initConfig,
618:                        methRepr.getContainingClass().getRootDirectory());
619:                return ProofAggregate.createProofAggregate(new Proof(name(),
620:                        proofObl, s, initConfig.createTacletIndex(), initConfig
621:                                .createBuiltInRuleIndex(), initConfig
622:                                .getServices()), name());
623:            }
624:
625:            /** sets the initial configuration that is used to read the OCL
626:             * input and that is used to be modified during reading.
627:             */
628:            public void setInitConfig(InitConfig conf) {
629:                this .initConfig = conf;
630:                initConfig.sortNS().startProtocol();
631:                initConfig.funcNS().startProtocol();
632:                initConfig.progVarNS().startProtocol();
633:            }
634:
635:            /** returns the name of the modifies check proof obligation input.
636:             */
637:            public String name() {
638:                return name;
639:            }
640:
641:            public void readActivatedChoices() throws ProofInputException {
642:
643:            }
644:
645:            /** reads the include section and returns an Includes object.  
646:             */
647:            public Includes readIncludes() throws ProofInputException {
648:                RuleSource standard = RuleSource
649:                        .initRuleFile("standardRules.key");
650:                Includes includes = new Includes();
651:                includes.put("standardRules", standard);
652:                return includes;
653:            }
654:
655:            public void readSpecs() {
656:                // nothing here
657:            }
658:
659:            public Term getPOTerm() {
660:                return proofObl;
661:            }
662:
663:            public SetOfTerm getModifiesElements() {
664:                return modifiesElements;
665:            }
666:
667:            public Contractable[] getObjectOfContract() {
668:                return new Contractable[] { methRepr };
669:            }
670:
671:            public boolean initContract(Contract ct) {
672:                return false; //%%
673:            }
674:
675:            public void startProtocol() {
676:                // do nothing
677:            }
678:
679:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.