Source Code Cross Referenced for TestGenerator.java in  » Testing » KeY » de » uka » ilkd » key » unittest » 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.unittest 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


0001:        // This file is part of KeY - Integrated Deductive Software Design
0002:        // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003:        //                         Universitaet Koblenz-Landau, Germany
0004:        //                         Chalmers University of Technology, Sweden
0005:        //
0006:        // The KeY system is protected by the GNU General Public License. 
0007:        // See LICENSE.TXT for details.
0008:        package de.uka.ilkd.key.unittest;
0009:
0010:        import de.uka.ilkd.key.java.*;
0011:        import de.uka.ilkd.key.java.declaration.*;
0012:        import de.uka.ilkd.key.java.declaration.modifier.*;
0013:        import de.uka.ilkd.key.java.expression.*;
0014:        import de.uka.ilkd.key.java.expression.operator.*;
0015:        import de.uka.ilkd.key.java.expression.literal.*;
0016:        import de.uka.ilkd.key.java.reference.*;
0017:        import de.uka.ilkd.key.java.abstraction.*;
0018:        import de.uka.ilkd.key.java.statement.*;
0019:        import de.uka.ilkd.key.java.visitor.*;
0020:        import de.uka.ilkd.key.util.*;
0021:        import de.uka.ilkd.key.visualdebugger.VisualDebugger;
0022:        import de.uka.ilkd.key.logic.*;
0023:        import de.uka.ilkd.key.logic.sort.*;
0024:        import de.uka.ilkd.key.logic.op.*;
0025:        import de.uka.ilkd.key.rule.soundness.TermProgramVariableCollector;
0026:        import de.uka.ilkd.key.rule.UpdateSimplifier;
0027:
0028:        import java.io.*;
0029:        import java.util.*;
0030:
0031:        /**
0032:         * Generates a unittest for a given piece of code and a set of modelgenerators.
0033:         */
0034:        public class TestGenerator {
0035:
0036:            private StringWriter w;
0037:            private Services serv;
0038:            private JavaInfo ji;
0039:
0040:            private KeYJavaType testCase;
0041:            private KeYJavaType testSuite;
0042:            private KeYJavaType b;
0043:            private KeYJavaType intType;
0044:            private Type suiteType;
0045:            private TypeRef testTypeRef;
0046:            private String fileName;
0047:            private String path = null;
0048:
0049:            private Random rand;
0050:
0051:            private MethodDeclaration suiteMethod;
0052:
0053:            private int mcounter = 0;
0054:
0055:            private MethodReference oracle = null;
0056:
0057:            static int counter = 0;
0058:
0059:            private HashMap translatedFormulas;
0060:            private String directory = System.getProperty("user.home")
0061:                    + File.separator + "testFiles";
0062:
0063:            //    private HashMap array2length;
0064:
0065:            /**
0066:             * creates a TestGenerator instance for the given compilation unit
0067:             * @param serv the Services
0068:             * @param fileName the name of the unittest file this TestGenerator 
0069:             * creates.
0070:             */
0071:            public TestGenerator(Services serv, String fileName) {
0072:                ji = serv.getJavaInfo();
0073:                translatedFormulas = new HashMap();
0074:                //	array2length = new HashMap();
0075:                this .fileName = fileName;
0076:                w = new StringWriter();
0077:                this .serv = serv;
0078:                ExtList l = new ExtList();
0079:                l.add(new ProgramElementName(fileName));
0080:                suiteType = new ClassDeclaration(l, new ProgramElementName(
0081:                        fileName), false);
0082:                KeYJavaType testType = new KeYJavaType(suiteType,
0083:                        new ClassInstanceSortImpl(new Name(fileName), false));
0084:                testTypeRef = new TypeRef(testType);
0085:                testCase = ji
0086:                        .getKeYJavaTypeByClassName("junit.framework.TestCase");
0087:                testSuite = ji
0088:                        .getKeYJavaTypeByClassName("junit.framework.TestSuite");
0089:                b = ji.getTypeByName("boolean");
0090:                intType = ji.getTypeByName("int");
0091:                suiteMethod = createSuiteMethod();
0092:                rand = new Random();
0093:            }
0094:
0095:            public TestGenerator(Services serv, String fileName,
0096:                    String directory) {
0097:                this (serv, fileName);
0098:                if (directory != null)
0099:                    this .directory = directory;
0100:            }
0101:
0102:            /**
0103:             * Creates the class declaration of the unit test that should be exported
0104:             * to a file.
0105:             */
0106:            private ClassDeclaration createSuiteClass(ExtList l) {
0107:                l.add(new Public());
0108:                l.add(new Extends(new TypeRef(testCase)));
0109:                l.add(new ProgramElementName(fileName));
0110:                ClassDeclaration result = new ClassDeclaration(l,
0111:                        new ProgramElementName(fileName), false);
0112:                //	FieldReplaceVisitor frv = new FieldReplaceVisitor(result);
0113:                //	frv.start();
0114:                return result;
0115:            }
0116:
0117:            private KeYJavaType getArrayTypeAndEnsureExistence(
0118:                    KeYJavaType baseType, int dim) {
0119:                final JavaInfo ji = serv.getJavaInfo();
0120:                Sort as = ArraySortImpl.getArraySortForDim(baseType.getSort(),
0121:                        dim, ji.getJavaLangObjectAsSort(), ji
0122:                                .getJavaLangCloneableAsSort(), ji
0123:                                .getJavaIoSerializableAsSort());
0124:                KeYJavaType kjt = ji.getKeYJavaType(as);
0125:                if (kjt == null || baseType.getSort().toString().equals("int")) {
0126:                    JavaBlock jb = ji.readJavaBlock("{" + as + " v;}");
0127:                    return ((VariableDeclaration) ((StatementBlock) jb
0128:                            .program()).getChildAt(0)).getTypeReference()
0129:                            .getKeYJavaType();
0130:                }
0131:                return kjt;
0132:            }
0133:
0134:            private KeYJavaType getBaseType(KeYJavaType arrayType) {
0135:                return ((ArrayType) arrayType.getJavaType()).getBaseType()
0136:                        .getKeYJavaType();
0137:            }
0138:
0139:            /** Creates a method of the form: 
0140:             *  public void <name>(){
0141:             *    &lt pv-decls for v0,...,vl &gt;
0142:             *    testData0 = {d_00,...,d_0k};
0143:             *    ...
0144:             *    testDataj = {d_j0,...,d_jk};
0145:             *    for(int i=0; i<testData0.length; i++){
0146:             *        ...
0147:             *        l0 = testData0[i];
0148:             *        ...
0149:             *        lj = testDataj[i];
0150:             *        <code>
0151:             *        java.lang.StringBuffer buffer;
0152:             *        buffer = new java.lang.StringBuffer ();
0153:             *	      boolean result = testOracle(v0,..., vl, buffer);
0154:             *        assertTrue (&lt String &gt, result);
0155:             *    }
0156:             *  }
0157:             *  Where &lt String &gt contains the assignments of l0,...,lj in this
0158:             *  iteration and the results the oracles for the subformulas of post
0159:             *  have provided so far.
0160:             *
0161:             */
0162:            private MethodDeclaration createTestMethod(Statement code[],
0163:                    Term post,
0164:                    Expression[][] testLocation,
0165:                    Expression[][] testData,
0166:                    //					       ProgramVariable[] pvs,
0167:                    ProgramVariable[] pvsNotDecl, String name,
0168:                    ExtList children, ModelGenerator mg,
0169:                    EquivalenceClass[] testLocEqvs) {
0170:                ListOfStatement s = SLListOfStatement.EMPTY_LIST;
0171:                // declare and initialize program variables
0172:                for (int i = 0; i < pvsNotDecl.length; i++) {
0173:                    VariableSpecification varSpec = null;
0174:                    if (pvsNotDecl[i].getKeYJavaType().getSort().extendsTrans(
0175:                            serv.getTypeConverter().getIntegerLDT()
0176:                                    .targetSort())) {
0177:                        varSpec = new VariableSpecification(pvsNotDecl[i],
0178:                                new TypeCast(new IntLiteral(0), new TypeRef(
0179:                                        pvsNotDecl[i].getKeYJavaType())),
0180:                                pvsNotDecl[i].getKeYJavaType());
0181:                    } else if (pvsNotDecl[i].getKeYJavaType().getSort() == b
0182:                            .getSort()) {
0183:                        varSpec = new VariableSpecification(pvsNotDecl[i],
0184:                                BooleanLiteral.TRUE, pvsNotDecl[i]
0185:                                        .getKeYJavaType());
0186:                    } else {
0187:                        /*		varSpec = 
0188:                         new VariableSpecification(
0189:                         pvsNotDecl[i], new New(
0190:                         new Expression[0], 
0191:                         new TypeRef(pvsNotDecl[i].getKeYJavaType()), 
0192:                         null),
0193:                         pvsNotDecl[i].getKeYJavaType());*/
0194:                        varSpec = new VariableSpecification(pvsNotDecl[i],
0195:                                NullLiteral.NULL, pvsNotDecl[i]
0196:                                        .getKeYJavaType());
0197:                    }
0198:                    LocalVariableDeclaration lvd = new LocalVariableDeclaration(
0199:                            new TypeRef(pvsNotDecl[i].getKeYJavaType()),
0200:                            varSpec);
0201:                    s = s.append(lvd);
0202:                }
0203:
0204:                // put test data in array
0205:                ProgramVariable[] testArray = new ProgramVariable[testLocation.length];
0206:                boolean singleTuple = singleTuple(testData);
0207:                for (int i = 0; i < testData.length; i++) {
0208:                    KeYJavaType kjt = testLocEqvs[i].getKeYJavaType();
0209:                    if (singleTuple) {
0210:                        Expression testDatum;
0211:                        if (testData[i][0] != null) {
0212:                            testDatum = new TypeCast(testData[i][0],
0213:                                    new TypeRef(kjt));
0214:                        } else {
0215:                            testDatum = new TypeCast(new IntLiteral(rand
0216:                                    .nextInt()), new TypeRef(kjt));
0217:                        }
0218:                        testArray[i] = new LocationVariable(
0219:                                new ProgramElementName("testData" + i), kjt);
0220:                        VariableSpecification vs = new VariableSpecification(
0221:                                testArray[i], testDatum, kjt.getJavaType());
0222:                        s = s.append(new LocalVariableDeclaration(new TypeRef(
0223:                                kjt), vs));
0224:                    } else {
0225:                        KeYJavaType akjt = getArrayTypeAndEnsureExistence(kjt,
0226:                                1);
0227:                        ExtList ai = new ExtList();
0228:                        for (int j = 0; j < testData[i].length; j++) {
0229:                            ExtList partj = new ExtList();
0230:                            if (testData[i][j] != null) {
0231:                                ai.add(new TypeCast(testData[i][j],
0232:                                        new TypeRef(kjt)));
0233:                            } else {
0234:                                ai.add(new TypeCast(new IntLiteral(rand
0235:                                        .nextInt()), new TypeRef(kjt)));
0236:                            }
0237:                        }
0238:                        testArray[i] = new LocationVariable(
0239:                                new ProgramElementName("testData" + i), akjt);
0240:                        ExtList aType = new ExtList();
0241:                        aType.add(new TypeRef(kjt));
0242:                        NewArray init = new NewArray(aType, kjt,
0243:                                new ArrayInitializer(ai), 1);
0244:                        VariableSpecification vs = new VariableSpecification(
0245:                                testArray[i], init, akjt.getJavaType());
0246:                        s = s.append(new LocalVariableDeclaration(new TypeRef(
0247:                                akjt), vs));
0248:                    }
0249:                }
0250:                ArrayOfExpression arg = new ArrayOfExpression();
0251:                ExtList l = new ExtList();
0252:                l.add(new ProgramElementName(name));
0253:                l.add(new Public());
0254:                Statement[] ib = new Statement[6 + code.length];
0255:
0256:                ProgramVariable partCounter = new LocationVariable(
0257:                        new ProgramElementName("testDataCounter"), intType);
0258:                ProgramVariable length = new LocationVariable(
0259:                        new ProgramElementName("length"), intType);
0260:
0261:                // assignments of test data to locations + initialization of 
0262:                // object references
0263:                ListOfStatement assignments = SLListOfStatement.EMPTY_LIST;
0264:
0265:                // initialization of arrays and creation of test data assignments
0266:                HashMap array2Cons = new HashMap();
0267:                ListOfStatement testDataAssignments = SLListOfStatement.EMPTY_LIST;
0268:                for (int i = 0; i < testData.length; i++) {
0269:                    for (int k = 0; k < testLocation[i].length; k++) {
0270:                        Expression testDat = singleTuple ? (Expression) testArray[i]
0271:                                : (Expression) new ArrayReference(testArray[i],
0272:                                        new Expression[] { partCounter });
0273:                        if (testLocation[i][k] instanceof  FieldReference
0274:                                && ((FieldReference) testLocation[i][k])
0275:                                        .getProgramVariable().name().toString()
0276:                                        .equals("length")) {
0277:                            KeYJavaType at = ((Expression) ((FieldReference) testLocation[i][k])
0278:                                    .getReferencePrefix()).getKeYJavaType(serv,
0279:                                    null);
0280:                            if (at.getSort() instanceof  ArraySort) {
0281:                                NewArray ar = new NewArray(
0282:                                        new Expression[] { testDat },
0283:                                        new TypeRef(getBaseType(at)), at, null,
0284:                                        0);
0285:                                //			array2length.put(((FieldReference) testLocation[i][k]).
0286:                                //					 getReferencePrefix().toString(), 
0287:                                //					 testDat);
0288:                                array2Cons.put(
0289:                                        ((FieldReference) testLocation[i][k])
0290:                                                .getReferencePrefix()
0291:                                                .toString(), ar);
0292:                                continue;
0293:                            }
0294:                        }
0295:                        IndexReplaceVisitor irv = new IndexReplaceVisitor(
0296:                                testLocation[i][k], testLocation, singleTuple,
0297:                                partCounter, testArray);
0298:                        irv.start();
0299:                        irv.result();
0300:                        testDataAssignments = testDataAssignments
0301:                                .append(assignmentOrSet((Expression) irv
0302:                                        .result(), testDat, serv));
0303:                    }
0304:                }
0305:
0306:                // initialization of other object references
0307:                EquivalenceClass[] nonPrim = mg
0308:                        .getNonPrimitiveLocationEqvClasses();
0309:                HashMap loc2cons = new HashMap();
0310:                LinkedList locationsOrdered = new LinkedList();
0311:                for (int i = 0; i < nonPrim.length; i++) {
0312:                    SetOfTerm locs = nonPrim[i].getLocations();
0313:                    IteratorOfTerm itt = locs.iterator();
0314:                    if (!nonPrim[i].isNull()) {
0315:                        Term nonPrimLocTerm = itt.next();
0316:                        Expression loc1 = translateTerm(nonPrimLocTerm, null,
0317:                                null);
0318:                        Expression cons;
0319:                        if (nonPrimLocTerm.sort() instanceof  ArraySort) {
0320:                            cons = (Expression) array2Cons.get(loc1.toString());
0321:                            if (cons == null) {
0322:                                KeYJavaType locKJT = nonPrim[i]
0323:                                        .getKeYJavaType();
0324:                                cons = new NewArray(
0325:                                        new Expression[] { new IntLiteral(20) },
0326:                                        new TypeRef(getBaseType(locKJT)),
0327:                                        locKJT, null, 0);
0328:                            }
0329:                            /*		    KeYJavaType locKJT =loc1.getKeYJavaType(serv, null);
0330:                             ExtList aType = new ExtList();
0331:                             aType.add(new TypeRef(locKJT));
0332:                             cons = new NewArray(aType, locKJT, 
0333:                             new ArrayInitializer(new ExtList()),
0334:                             0);*/
0335:                        } else {
0336:                            cons = new New(new Expression[0], new TypeRef(
0337:                                    nonPrim[i].getKeYJavaType()), null);
0338:                        }
0339:                        if (locs.size() > 1) {
0340:                            ProgramVariable pv = new LocationVariable(
0341:                                    new ProgramElementName("_init" + i),
0342:                                    nonPrim[i].getKeYJavaType());
0343:                            VariableSpecification varSpec = new VariableSpecification(
0344:                                    pv, cons, nonPrim[i].getKeYJavaType());
0345:                            assignments = assignments
0346:                                    .append(new LocalVariableDeclaration(
0347:                                            new TypeRef(nonPrim[i]
0348:                                                    .getKeYJavaType()), varSpec));
0349:                            loc2cons.put(loc1, pv);
0350:                            while (itt.hasNext()) {
0351:                                Expression loc2 = translateTerm(itt.next(),
0352:                                        null, null);
0353:                                addOrdered(loc2, locationsOrdered);
0354:                                loc2cons.put(loc2, pv);
0355:                            }
0356:                        } else {
0357:                            loc2cons.put(loc1, cons);
0358:                        }
0359:                        addOrdered(loc1, locationsOrdered);
0360:                    } else {
0361:                        while (itt.hasNext()) {
0362:                            Term locTerm = itt.next();
0363:                            if (locTerm.op() != Op.NULL) {
0364:                                Expression loc2 = translateTerm(locTerm, null,
0365:                                        null);
0366:                                addOrdered(loc2, locationsOrdered);
0367:                                loc2cons.put(loc2, NullLiteral.NULL);
0368:                            }
0369:                        }
0370:                    }
0371:                }
0372:                Iterator locIt = locationsOrdered.iterator();
0373:                while (locIt.hasNext()) {
0374:                    Expression loc = (Expression) locIt.next();
0375:                    Expression cons = (Expression) loc2cons.get(loc);
0376:                    IndexReplaceVisitor irv = new IndexReplaceVisitor(loc,
0377:                            testLocation, singleTuple, partCounter, testArray);
0378:                    irv.start();
0379:                    irv.result();
0380:                    assignments = assignments.append(assignmentOrSet(
0381:                            (Expression) irv.result(), cons, serv));
0382:                }
0383:
0384:                assignments = assignments.append(testDataAssignments);
0385:                //	assignments = removeOutOfBounds(assignments);
0386:                ib[0] = new StatementBlock(assignments.toArray());
0387:
0388:                for (int i = 0; i < code.length; i++) {
0389:                    ib[i + 1] = code[i];
0390:                }
0391:
0392:                KeYJavaType sb = ji
0393:                        .getKeYJavaTypeByClassName("java.lang.StringBuffer");
0394:                New cons = new New(new Expression[0], new TypeRef(sb), null);
0395:                ProgramVariable buffer = new LocationVariable(
0396:                        new ProgramElementName("buffer"), sb);
0397:                ib[code.length + 1] = new LocalVariableDeclaration(new TypeRef(
0398:                        sb), new VariableSpecification(buffer));
0399:                ib[code.length + 2] = new CopyAssignment(buffer, cons);
0400:
0401:                ProgramVariable result = new LocationVariable(
0402:                        new ProgramElementName("result"), b);
0403:                ib[code.length + 3] = new LocalVariableDeclaration(new TypeRef(
0404:                        b), new VariableSpecification(result));
0405:                MethodReference oracle = getOracle(post, buffer, children);
0406:                ib[code.length + 4] = new CopyAssignment(result, oracle);
0407:                ProgramMethod assertTrue = ji
0408:                        .getProgramMethod(
0409:                                testCase,
0410:                                "assertTrue",
0411:                                SLListOfKeYJavaType.EMPTY_LIST
0412:                                        .append(
0413:                                                ji
0414:                                                        .getKeYJavaTypeByClassName("java.lang.String"))
0415:                                        .append(b), testCase);
0416:                Expression failure = new StringLiteral(
0417:                        "\\nPost evaluated to false.\\n"
0418:                                + "Variable/Location Assignments:\\n");
0419:                for (int i = 0; i < testLocation.length; i++) {
0420:                    for (int j = 0; j < testLocation[i].length; j++) {
0421:                        Expression assignment = new Plus(
0422:                                new StringLiteral("  "
0423:                                        + testLocation[i][j].toString() + " = "),
0424:                                singleTuple ? (Expression) testArray[i]
0425:                                        : (Expression) new ArrayReference(
0426:                                                testArray[i],
0427:                                                new Expression[] { partCounter }));
0428:                        failure = new Plus(failure, assignment);
0429:                    }
0430:                }
0431:                Expression str = new Plus(new StringLiteral(
0432:                        "\\nEvaluation of subformulas so far: "),
0433:                        new MethodReference(new ArrayOfExpression(),
0434:                                new ProgramElementName("toString"), buffer));
0435:                str = new Plus(failure, str);
0436:                ib[code.length + 5] = new MethodReference(
0437:                        new ArrayOfExpression(new Expression[] { str, result }),
0438:                        new ProgramElementName("assertTrue"), null);
0439:
0440:                Statement body = new StatementBlock(ib);
0441:
0442:                // nested loops for executing the tested code with every possible 
0443:                // combination of testdata in each partition  
0444:                if (!singleTuple) {
0445:                    /*	    for(int i=0; i<testData.length; i++){
0446:                     VariableSpecification counterSpec = 
0447:                     new VariableSpecification(lCounter[i], new IntLiteral(0), 
0448:                     intType);
0449:                     LocalVariableDeclaration counterDecl = 
0450:                     new LocalVariableDeclaration(new TypeRef(intType),
0451:                     counterSpec);
0452:                     Expression guard = 
0453:                     new LessThan(lCounter[i], new FieldReference(
0454:                     length, new ArrayReference(
0455:                     testArray[i], 
0456:                     new Expression[]{partCounter})));
0457:                     Expression update = new PostIncrement(lCounter[i]);
0458:                     body = new For(new LoopInitializer[]{counterDecl}, guard, 
0459:                     new Expression[]{update}, body);
0460:                     }*/
0461:                    // loop over the number of partitions
0462:                    //	    int partCount = testData.length==0? 1 : testData[0].length;
0463:                    VariableSpecification counterSpec = new VariableSpecification(
0464:                            partCounter, new IntLiteral(0), intType);
0465:                    LocalVariableDeclaration counterDecl = new LocalVariableDeclaration(
0466:                            new TypeRef(intType), counterSpec);
0467:                    Expression guard = new LessThan(partCounter,
0468:                            testData.length == 0 ? (Expression) new IntLiteral(
0469:                                    1) : (Expression) new FieldReference(
0470:                                    length, testArray[0]));
0471:                    //	    Expression guard = 
0472:                    //		new LessThan(partCounter, new IntLiteral(partCount));
0473:                    Expression update = new PostIncrement(partCounter);
0474:                    body = new For(new LoopInitializer[] { counterDecl },
0475:                            guard, new Expression[] { update }, body);
0476:                }
0477:
0478:                s = s.append(body);
0479:                StatementBlock mBody = new StatementBlock(s.toArray());
0480:                FieldReplaceVisitor frv = new FieldReplaceVisitor(mBody);
0481:                frv.start();
0482:                l.add(frv.result());
0483:                l.add(new Comment("\n  Covered execution trace:\n"
0484:                        + mg.getExecutionTrace()));
0485:                MethodDeclaration tm = new MethodDeclaration(l, false);
0486:
0487:                if (VisualDebugger.isDebuggingMode()) {
0488:                    VisualDebugger.getVisualDebugger().addTestCase(fileName,
0489:                            name, mg.getOriginalNode());
0490:                }
0491:
0492:                return tm;
0493:            }
0494:
0495:            private void addOrdered(Expression e, LinkedList l) {
0496:                for (int i = 0; i < l.size(); i++) {
0497:                    if (depth((Expression) l.get(i)) > depth(e)) {
0498:                        l.add(i, e);
0499:                        return;
0500:                    }
0501:                }
0502:                l.add(e);
0503:            }
0504:
0505:            private boolean singleTuple(Expression[][] e) {
0506:                if (0 < e.length) {
0507:                    return e[0].length == 1;
0508:                }
0509:                return true;
0510:            }
0511:
0512:            /**
0513:             * Returns the depth, i.e. the length of the reference prefix of an
0514:             * expression.
0515:             */
0516:            private int depth(Expression e) {
0517:                if ((e instanceof  FieldReference)
0518:                        && (((FieldReference) e).getReferencePrefix() instanceof  Expression)) {
0519:                    return 1 + depth((Expression) ((FieldReference) e)
0520:                            .getReferencePrefix());
0521:                } else if ((e instanceof  ArrayReference)
0522:                        && (((ArrayReference) e).getReferencePrefix() instanceof  Expression)) {
0523:                    return depth((Expression) ((ArrayReference) e)
0524:                            .getReferencePrefix()) + 1;
0525:                }
0526:                return 0;
0527:            }
0528:
0529:            /**
0530:             * Generates either an assignment statement lhs = rhs; or a method call
0531:             * statement for the appropriate set method in the case that
0532:             * lhs is a field reference.
0533:             */
0534:            public static Statement assignmentOrSet(Expression lhs,
0535:                    Expression rhs, Services serv) {
0536:                if (lhs instanceof  FieldReference) {
0537:                    ProgramVariable pv = ((FieldReference) lhs)
0538:                            .getProgramVariable();
0539:                    String typeName = pv.getKeYJavaType().getName();
0540:                    typeName = PrettyPrinter
0541:                            .getTypeNameForAccessMethods(typeName);
0542:                    KeYJavaType kjt = pv.getContainerType();
0543:                    String pvName = pv.name().toString();
0544:                    pvName = pvName.substring(pvName.lastIndexOf(":") + 1);
0545:                    String methodName = "_set" + pvName + typeName;
0546:                    ListOfKeYJavaType sig = SLListOfKeYJavaType.EMPTY_LIST;
0547:                    sig = sig.append(pv.getKeYJavaType());
0548:                    return new MethodReference(new ArrayOfExpression(rhs),
0549:                            new ProgramElementName(methodName),
0550:                            ((FieldReference) lhs).getReferencePrefix());
0551:                }
0552:                CopyAssignment ca = new CopyAssignment(lhs, rhs);
0553:                if (lhs instanceof  ArrayReference) {
0554:                    KeYJavaType ae = serv.getJavaInfo()
0555:                            .getKeYJavaTypeByClassName(
0556:                                    "java.lang.ArrayIndexOutOfBoundsException");
0557:                    ParameterDeclaration pd = new ParameterDeclaration(
0558:                            new Modifier[0], new TypeRef(ae),
0559:                            new VariableSpecification(new LocationVariable(
0560:                                    new ProgramElementName("e"), ae)), false);
0561:                    Branch c = new Catch(pd, new StatementBlock());
0562:                    return new Try(new StatementBlock(ca), new Branch[] { c });
0563:                } else {
0564:                    return ca;
0565:                }
0566:            }
0567:
0568:            /**
0569:             * creates the method public static junit.framework.TestSuite suite () ...
0570:             * which is needed for junit test suites.
0571:             */
0572:            private MethodDeclaration createSuiteMethod() {
0573:                TypeRef testSuiteRef = new TypeRef(testSuite);
0574:                ExtList l = new ExtList();
0575:                l.add(new ProgramElementName("suite"));
0576:                l.add(new Public());
0577:                l.add(new Static());
0578:                l.add(testSuiteRef);
0579:                Statement[] s = new Statement[3];
0580:
0581:                ProgramVariable suite = new LocationVariable(
0582:                        new ProgramElementName("suite"), testSuite);
0583:                s[0] = new LocalVariableDeclaration(testSuiteRef,
0584:                        new VariableSpecification(suite));
0585:                Expression[] arg = new Expression[1];
0586:                arg[0] = new MetaClassReference(testTypeRef);
0587:                New cons = new New(arg, testSuiteRef, null);
0588:                s[1] = new CopyAssignment(suite, cons);
0589:                s[2] = new Return(suite);
0590:                StatementBlock mBody = new StatementBlock(s);
0591:                FieldReplaceVisitor frv = new FieldReplaceVisitor(mBody);
0592:                frv.start();
0593:                l.add(frv.result());
0594:                return new MethodDeclaration(l, false);
0595:            }
0596:
0597:            /**
0598:             * Generates the testcase and writes it to a file.
0599:             * @param code the piece of code that is tested by the generated unittest.
0600:             * @param oracle a term representing the postcondition of 
0601:             *         <code>code</code>. It is used to create a testoracle.
0602:             * @param mgs List of ModelGenerators.
0603:             * @param programVars program variables that have to be declared in the 
0604:             *         method.
0605:             * @param methodName the name of the testmethod created for 
0606:             *         <code>code</code>within the test case.
0607:             */
0608:            public void generateTestSuite(Statement[] code, Term oracle,
0609:                    List mgs, SetOfProgramVariable programVars,
0610:                    String methodName, PackageReference pr) {
0611:                UpdateSimplifier simplifier = new UpdateSimplifier();
0612:                oracle = simplifier.simplify(oracle, serv);
0613:                HashSet processedModels = new HashSet();
0614:                int dm = 0;
0615:                Iterator it = mgs.iterator();
0616:                //	ProgramVariable[] pva = null;
0617:                ProgramVariable[] pvaNotDecl = null;
0618:                while (it.hasNext()) {
0619:                    ModelGenerator mg = (ModelGenerator) it.next();
0620:                    programVars = programVars.union(mg.getProgramVariables());
0621:                }
0622:                pvaNotDecl = removeDublicates(programVars).toArray();
0623:                it = mgs.iterator();
0624:                ExtList l = new ExtList();
0625:                l.add(suiteMethod);
0626:                int testMCounter = 0;
0627:                while (it.hasNext()) {
0628:                    ModelGenerator mg = (ModelGenerator) it.next();
0629:                    Model[] models = mg.createModels();
0630:                    int dublicate = 0;
0631:                    if (models.length - dublicate == 0 && mgs.size() != 1) {
0632:                        continue;
0633:                    }
0634:                    EquivalenceClass[] eqvArray = mg
0635:                            .getPrimitiveLocationEqvClasses();
0636:                    Expression[][] testLocation = new Expression[eqvArray.length][];
0637:                    Expression[][] testData = new Expression[eqvArray.length][models.length
0638:                            - dublicate];
0639:                    for (int i = 0; i < eqvArray.length; i++) {
0640:                        SetOfTerm locs = eqvArray[i].getLocations();
0641:                        testLocation[i] = new Expression[locs.size()];
0642:                        int k = 0;
0643:                        IteratorOfTerm itt = locs.iterator();
0644:                        while (itt.hasNext()) {
0645:                            Term testLoc = itt.next();
0646:                            testLocation[i][k++] = translateTerm(testLoc, null,
0647:                                    null);
0648:                        }
0649:                        for (int j = 0; j < models.length - dublicate; j++) {
0650:                            testData[i][j] = models[j]
0651:                                    .getValueAsExpression(eqvArray[i]);
0652:                        }
0653:                    }
0654:                    l.add(createTestMethod(code, oracle, testLocation,
0655:                            testData, pvaNotDecl,
0656:                            methodName + (testMCounter++), l, mg, eqvArray));
0657:                }
0658:
0659:                ClassDeclaration suite = createSuiteClass(l);
0660:                PrettyPrinter pp = new PrettyPrinter(w, false, true);
0661:                try {
0662:                    // write the file to disk
0663:                    pp.printClassDeclaration(suite);
0664:                    File dir = new File(directory);
0665:                    if (!dir.exists()) {
0666:                        dir.mkdirs();
0667:                    }
0668:                    File pcFile = new File(dir, fileName + ".java");
0669:                    path = pcFile.getAbsolutePath();
0670:                    FileWriter fw = new FileWriter(pcFile);
0671:                    BufferedWriter bw = new BufferedWriter(fw);
0672:                    bw.write(addImports(clean(w.toString()), pr));
0673:                    bw.close();
0674:                } catch (IOException ioe) {
0675:                }
0676:                exportCodeUnderTest();
0677:            }
0678:
0679:            /**
0680:             * Exports the code under test to files and adds get and set methods for
0681:             * each field.
0682:             */
0683:            public void exportCodeUnderTest() {
0684:                Set kjts = ji.getAllKeYJavaTypes();
0685:                Iterator it = kjts.iterator();
0686:                while (it.hasNext()) {
0687:                    KeYJavaType kjt = (KeYJavaType) it.next();
0688:                    if ((kjt.getJavaType() instanceof  ClassDeclaration || kjt
0689:                            .getJavaType() instanceof  InterfaceDeclaration)
0690:                            && ((TypeDeclaration) kjt.getJavaType())
0691:                                    .getPositionInfo().getFileName() != null
0692:                            && ((TypeDeclaration) kjt.getJavaType())
0693:                                    .getPositionInfo().getFileName().indexOf(
0694:                                            "resources") == -1) {
0695:
0696:                        StringWriter sw = new StringWriter();
0697:                        PrettyPrinter pp = new PrettyPrinter(sw, false, true);
0698:                        try {
0699:                            // write the implementation under test to the testFiles
0700:                            // directory
0701:                            if (kjt.getJavaType() instanceof  ClassDeclaration) {
0702:                                pp.printClassDeclaration((ClassDeclaration) kjt
0703:                                        .getJavaType());
0704:                            } else {
0705:                                pp
0706:                                        .printInterfaceDeclaration((InterfaceDeclaration) kjt
0707:                                                .getJavaType());
0708:                            }
0709:                            String fn = ((TypeDeclaration) kjt.getJavaType())
0710:                                    .getPositionInfo().getFileName();
0711:
0712:                            String header = getHeader(fn);
0713:
0714:                            File dir = new File(directory
0715:                                    + fn.substring(0, fn
0716:                                            .lastIndexOf(File.separator)));
0717:                            fn = fn
0718:                                    .substring(fn.lastIndexOf(File.separator) + 1);
0719:                            if (!dir.exists()) {
0720:                                dir.mkdirs();
0721:                            }
0722:                            File pcFile = new File(dir, fn);
0723:                            FileWriter fw = new FileWriter(pcFile);
0724:                            BufferedWriter bw = new BufferedWriter(fw);
0725:                            bw.write(header);
0726:                            bw.write(clean(sw.toString()));
0727:                            bw.close();
0728:                        } catch (IOException ioe) {
0729:                            throw new UnitTestException(ioe);
0730:                        }
0731:                    }
0732:                }
0733:            }
0734:
0735:            private String clean(String s) {
0736:                while (s.indexOf(";.") != -1) {
0737:                    s = s.substring(0, s.indexOf(";."))
0738:                            + s.substring(s.indexOf(";.") + 1);
0739:                }
0740:                while (s.indexOf(";;") != -1) {
0741:                    s = s.substring(0, s.indexOf(";;"))
0742:                            + s.substring(s.indexOf(";;") + 1);
0743:                }
0744:                while (s.indexOf(";[") != -1) {
0745:                    s = s.substring(0, s.indexOf(";["))
0746:                            + s.substring(s.indexOf(";[") + 1);
0747:                }
0748:                while (s.indexOf(";]") != -1) {
0749:                    s = s.substring(0, s.indexOf(";]"))
0750:                            + s.substring(s.indexOf(";]") + 1);
0751:                }
0752:                return s;
0753:            }
0754:
0755:            /** Returns the header consisting of package and import statements 
0756:             * occuring in the file <code>fileName</code>.
0757:             */
0758:            private String getHeader(String fileName) {
0759:                String result = "";
0760:                String lineSeparator = System.getProperty("line.separator");
0761:                BufferedReader reader;
0762:                try {
0763:                    reader = new BufferedReader(new FileReader(fileName));
0764:                    String line;
0765:                    while ((line = reader.readLine()) != null) {
0766:                        result += line + lineSeparator;
0767:                    }
0768:                    reader.close();
0769:                } catch (IOException ioe) {
0770:                    throw new UnitTestException(ioe);
0771:                }
0772:                int declIndex = result.indexOf("class ");
0773:                if (declIndex == -1) {
0774:                    declIndex = result.indexOf("interface ");
0775:                }
0776:                result = result.substring(0, declIndex);
0777:                result = result.substring(0, result.lastIndexOf(";") + 1);
0778:                return result + "\n\n";
0779:            }
0780:
0781:            public SetOfProgramVariable removeDublicates(
0782:                    SetOfProgramVariable pvs) {
0783:                HashSet names = new HashSet();
0784:                IteratorOfProgramVariable it = pvs.iterator();
0785:                SetOfProgramVariable result = SetAsListOfProgramVariable.EMPTY_SET;
0786:                while (it.hasNext()) {
0787:                    ProgramVariable pv = it.next();
0788:                    if (names.add(pv.name().toString())) {
0789:                        result = result.add(pv);
0790:                    }
0791:                }
0792:                return result;
0793:            }
0794:
0795:            /** 
0796:             * Returns the path of the file generated by this instance.
0797:             */
0798:            public String getPath() {
0799:                return path;
0800:            }
0801:
0802:            private String addImports(String classDec, PackageReference pr) {
0803:                String imports = "import junit.framework.*;";
0804:                if (pr != null) {
0805:                    imports += "\nimport " + pr + ".*;";
0806:                }
0807:                return imports + "\n\n" + classDec;
0808:            }
0809:
0810:            /** Creates a testoracle from the term <code>post</code>.
0811:             * @param post the term used for creating a testoracle.
0812:             * @param buffer a program variable of type StringBuffer.
0813:             * @param children the children of the enclosing class. The MethodDeclarations 
0814:             *       created by this method are added to <code>children</code>.
0815:             */
0816:            public MethodReference getOracle(Term post, ProgramVariable buffer,
0817:                    ExtList children) {
0818:                if (oracle == null) {
0819:                    post = replaceConstants(post, serv, null);
0820:                    oracle = (MethodReference) getMethodReferenceForFormula(
0821:                            post, buffer, children);
0822:                }
0823:                return oracle;
0824:            }
0825:
0826:            /**
0827:             * Returns the method reference the term post is translated to and creates
0828:             * also the corresponding method declaration.
0829:             */
0830:            private Expression getMethodReferenceForFormula(Term post,
0831:                    ProgramVariable buffer, ExtList children) {
0832:                if (post.sort() != Sort.FORMULA) {
0833:                    return translateTerm(post, buffer, children);
0834:                }
0835:                if (translatedFormulas.containsKey(post)) {
0836:                    return (Expression) translatedFormulas.get(post);
0837:                }
0838:                ExtList args = getArguments(post);
0839:                args.add(buffer);
0840:                LinkedList params = getParameterDeclarations(args);
0841:                Statement[] mBody = buildMethodBodyFromFormula(post, buffer,
0842:                        children);
0843:                MethodDeclaration md = buildMethodDeclaration(mBody,
0844:                        new TypeRef(b), "subformula", params);
0845:                children.add(md);
0846:                MethodReference mr = new MethodReference(args,
0847:                        new ProgramElementName(md.getName()), testTypeRef);
0848:                translatedFormulas.put(post, mr);
0849:                return mr;
0850:            }
0851:
0852:            /**
0853:             * Creates the method body for the method the term post is translated to.
0854:             */
0855:            private Statement[] buildMethodBodyFromFormula(Term post,
0856:                    ProgramVariable buffer, ExtList children) {
0857:                Statement[] s = new Statement[4];
0858:                ProgramVariable result = new LocationVariable(
0859:                        new ProgramElementName("result"), b);
0860:                s[0] = new LocalVariableDeclaration(new TypeRef(b),
0861:                        new VariableSpecification(result));
0862:                Expression f = translateFormula(post, buffer, children);
0863:                s[1] = new CopyAssignment(result, f);
0864:                Plus str = new Plus(new StringLiteral("\\neval(" + post
0865:                        + ") = "), result);
0866:                s[2] = new MethodReference(new ArrayOfExpression(str),
0867:                        new ProgramElementName("append"), buffer);
0868:                s[3] = new Return(result);
0869:                return s;
0870:            }
0871:
0872:            /**
0873:             * Translates a term to a java expression. 
0874:             */
0875:            private Expression translateTerm(Term t, ProgramVariable buffer,
0876:                    ExtList children) {
0877:                Expression result = null;
0878:                if (t.op() instanceof  ProgramInLogic) {
0879:                    final ExtList tchildren = new ExtList();
0880:                    for (int i = 0; i < t.arity(); i++) {
0881:                        tchildren
0882:                                .add(translateTerm(t.sub(i), buffer, children));
0883:                    }
0884:                    return ((ProgramInLogic) t.op()).convertToProgram(t,
0885:                            tchildren);
0886:                } else if (t.op() == Op.IF_THEN_ELSE) {
0887:                    ExtList l = new ExtList();
0888:                    l.add(getMethodReferenceForFormula(t.sub(0), buffer,
0889:                            children));
0890:                    l.add(translateTerm(t.sub(1), buffer, children));
0891:                    l.add(translateTerm(t.sub(2), buffer, children));
0892:                    result = new Conditional(l);
0893:                    result = new ParenthesizedExpression(result);
0894:                } else if (t.op() instanceof  Function) {
0895:                    String name = t.op().name().toString().intern();
0896:                    if (name.equals("add") || name.equals("jadd")
0897:                            || name.equals("addJint")) {
0898:                        result = new Plus(translateTerm(t.sub(0), buffer,
0899:                                children), translateTerm(t.sub(1), buffer,
0900:                                children));
0901:                    } else if (name.equals("sub") || name.equals("jsub")
0902:                            || name.equals("subJint")) {
0903:                        result = new Minus(translateTerm(t.sub(0), buffer,
0904:                                children), translateTerm(t.sub(1), buffer,
0905:                                children));
0906:                    } else if (name.equals("neg") || name.equals("jneg")
0907:                            || name.equals("negJint") || name.equals("neglit")) {
0908:                        result = new Negative(translateTerm(t.sub(0), buffer,
0909:                                children));
0910:                    } else if (name.equals("mul") || name.equals("jmul")
0911:                            || name.equals("mulJint")) {
0912:                        result = new Times(translateTerm(t.sub(0), buffer,
0913:                                children), translateTerm(t.sub(1), buffer,
0914:                                children));
0915:                    } else if (name.equals("div") || name.equals("jdiv")
0916:                            || name.equals("divJint")) {
0917:                        result = new Divide(translateTerm(t.sub(0), buffer,
0918:                                children), translateTerm(t.sub(1), buffer,
0919:                                children));
0920:                    } else if (name.equals("mod") || name.equals("jmod")
0921:                            || name.equals("modJint")) {
0922:                        result = new Modulo(translateTerm(t.sub(0), buffer,
0923:                                children), translateTerm(t.sub(1), buffer,
0924:                                children));
0925:                    } else if (name.equals("Z")) {
0926:                        result = translateTerm(t.sub(0), buffer, children);
0927:                    }
0928:                    if (result != null) {
0929:                        result = new ParenthesizedExpression(result);
0930:                    }
0931:                }
0932:                if (result == null) {
0933:                    result = convertToProgramElement(t);
0934:                }
0935:                return result;
0936:            }
0937:
0938:            /**
0939:             * Translates a formula to a java expression, i.e. an oracle for the 
0940:             * is created
0941:             * @param children the children of the enclosing class. The method 
0942:             *         declarations created by this method are added to <code>
0943:             *         children</code>.
0944:             */
0945:            private Expression translateFormula(Term post,
0946:                    ProgramVariable buffer, ExtList children) {
0947:                ExtList l = new ExtList();
0948:                if (post.sort() != Sort.FORMULA) {
0949:                    return translateTerm(post, buffer, children);
0950:                } else if (post.op() == Op.TRUE) {
0951:                    return BooleanLiteral.TRUE;
0952:                } else if (post.op() == Op.FALSE) {
0953:                    return BooleanLiteral.FALSE;
0954:                } else if (post.op() == Op.NOT) {
0955:                    l.add(new ParenthesizedExpression(translateFormula(post
0956:                            .sub(0), buffer, children)));
0957:                    return new LogicalNot(l);
0958:                } else if (post.op() == Op.AND) {
0959:                    return new LogicalAnd(getMethodReferenceForFormula(post
0960:                            .sub(0), buffer, children),
0961:                            getMethodReferenceForFormula(post.sub(1), buffer,
0962:                                    children));
0963:                } else if (post.op() == Op.OR) {
0964:                    return new LogicalOr(getMethodReferenceForFormula(post
0965:                            .sub(0), buffer, children),
0966:                            getMethodReferenceForFormula(post.sub(1), buffer,
0967:                                    children));
0968:                } else if (post.op() == Op.IMP) {
0969:                    l.add(getMethodReferenceForFormula(post.sub(0), buffer,
0970:                            children));
0971:                    return new LogicalOr(new LogicalNot(l),
0972:                            getMethodReferenceForFormula(post.sub(1), buffer,
0973:                                    children));
0974:                } else if (post.op() instanceof  Equality) {
0975:                    l.add(getMethodReferenceForFormula(post.sub(0), buffer,
0976:                            children));
0977:                    l.add(getMethodReferenceForFormula(post.sub(1), buffer,
0978:                            children));
0979:                    Equals eq = new Equals(l);
0980:                    return eq;
0981:                } else if (post.op() == Op.IF_THEN_ELSE) {
0982:                    l.add(getMethodReferenceForFormula(post.sub(0), buffer,
0983:                            children));
0984:                    l.add(getMethodReferenceForFormula(post.sub(1), buffer,
0985:                            children));
0986:                    l.add(getMethodReferenceForFormula(post.sub(2), buffer,
0987:                            children));
0988:                    return new Conditional(l);
0989:                } else if (post.op() == Op.ALL) {
0990:                    return translateQuantifiedTerm(true, post, buffer, children);
0991:                } else if (post.op() == Op.EX) {
0992:                    return translateQuantifiedTerm(false, post, buffer,
0993:                            children);
0994:                } else if (post.op().name().toString().equals("lt")) {
0995:                    return new LessThan(translateTerm(post.sub(0), buffer,
0996:                            children), translateTerm(post.sub(1), buffer,
0997:                            children));
0998:                } else if (post.op().name().toString().equals("gt")) {
0999:                    l.add(translateTerm(post.sub(0), buffer, children));
1000:                    l.add(translateTerm(post.sub(1), buffer, children));
1001:                    return new GreaterThan(l);
1002:                } else if (post.op().name().toString().equals("geq")) {
1003:                    l.add(translateTerm(post.sub(0), buffer, children));
1004:                    l.add(translateTerm(post.sub(1), buffer, children));
1005:                    return new GreaterOrEquals(l);
1006:                } else if (post.op().name().toString().equals("leq")) {
1007:                    return new LessOrEquals(translateTerm(post.sub(0), buffer,
1008:                            children), translateTerm(post.sub(1), buffer,
1009:                            children));
1010:                }
1011:                throw new NotTranslatableException(
1012:                        "Test oracle could not be generated");
1013:            }
1014:
1015:            /**
1016:             * Builds a method declaration with the provided name and type.
1017:             * Field references o.a occuring in the method body are replaced
1018:             * by methodcalls o._a().
1019:             */
1020:            private MethodDeclaration buildMethodDeclaration(Statement[] body,
1021:                    TypeRef type, String name, LinkedList params) {
1022:                ExtList l = new ExtList();
1023:                l.add(new ProgramElementName(name + (mcounter++)));
1024:                l.add(new Private());
1025:                l.add(new Static());
1026:                l.addAll(params);
1027:                l.add(type);
1028:                StatementBlock mBody = new StatementBlock(body);
1029:                FieldReplaceVisitor frv = new FieldReplaceVisitor(mBody);
1030:                frv.start();
1031:                l.add(frv.result());
1032:                MethodDeclaration md = new MethodDeclaration(l, false);
1033:                return md;
1034:            }
1035:
1036:            /**
1037:             * Creates an oracle for a quantified formula, which is only possible for 
1038:             * some classes of quantified formulas. If <code>t</code> doesn't belong
1039:             * to one of these classes a NotTranslatableException is thrown.
1040:             */
1041:            private Expression translateQuantifiedTerm(boolean all, Term t,
1042:                    ProgramVariable buffer, ExtList children) {
1043:                de.uka.ilkd.key.logic.op.Operator junctor;
1044:                Expression resInit;
1045:                if (all) {
1046:                    junctor = Op.IMP;
1047:                    resInit = BooleanLiteral.TRUE;
1048:                } else {
1049:                    junctor = Op.AND;
1050:                    resInit = BooleanLiteral.FALSE;
1051:                }
1052:                //	if(true ) return BooleanLiteral.TRUE;
1053:                Statement[] body = new Statement[4];
1054:                Expression[] bounds = new Expression[] { null, null, null, null };
1055:                LogicVariable lv = (LogicVariable) t.varsBoundHere(0)
1056:                        .lastQuantifiableVariable();
1057:                if (t.varsBoundHere(0).size() > 1
1058:                        || !(lv.sort() == intType.getSort() || lv.sort()
1059:                                .toString().equals("jint"))) {
1060:                    throw new NotTranslatableException("quantified Term " + t);
1061:                }
1062:                ProgramVariable result = new LocationVariable(
1063:                        new ProgramElementName("result"), b);
1064:                body[0] = new LocalVariableDeclaration(new TypeRef(b),
1065:                        new VariableSpecification(result, resInit, b
1066:                                .getJavaType()));
1067:                KeYJavaType lvType = intType;
1068:                ProgramVariable pv = new LocationVariable(
1069:                        new ProgramElementName("_" + lv.name() + (counter++)),
1070:                        lvType);
1071:                Term sub0 = replaceLogicVariable(t.sub(0), lv, pv);
1072:                if (sub0.op() == junctor && sub0.sub(0).op() == Op.AND) {
1073:                    Term range = sub0.sub(0);
1074:                    getBound(range.sub(0), bounds, pv, buffer, children);
1075:                    getBound(range.sub(1), bounds, pv, buffer, children);
1076:                } else if (sub0.op() == junctor && sub0.sub(1).op() == junctor) {
1077:                    getBound(sub0.sub(0), bounds, pv, buffer, children);
1078:                    getBound(sub0.sub(1).sub(0), bounds, pv, buffer, children);
1079:                } else {
1080:                    throw new NotTranslatableException("quantified Term " + t);
1081:                }
1082:
1083:                Statement loopBody = new CopyAssignment(result,
1084:                        all ? (Expression) new LogicalAnd(result,
1085:                                getMethodReferenceForFormula(sub0.sub(1),
1086:                                        buffer, children))
1087:                                : (Expression) new LogicalOr(result,
1088:                                        getMethodReferenceForFormula(sub0
1089:                                                .sub(1), buffer, children)));
1090:                VariableSpecification vs = new VariableSpecification(pv,
1091:                        bounds[0] != null ? bounds[0] : new Plus(bounds[1],
1092:                                new IntLiteral(1)), intType.getJavaType());
1093:                LocalVariableDeclaration init = new LocalVariableDeclaration(
1094:                        new TypeRef(intType), vs);
1095:                Expression guard = bounds[2] == null ? (Expression) new LessThan(
1096:                        pv, bounds[3])
1097:                        : (Expression) new LessOrEquals(pv, bounds[2]);
1098:                Expression update = new PostIncrement(pv);
1099:                body[1] = new For(new LoopInitializer[] { init }, guard,
1100:                        new Expression[] { update }, new StatementBlock(
1101:                                loopBody));
1102:                Plus str = new Plus(new StringLiteral("\\neval(" + t + ") = "),
1103:                        result);
1104:                body[2] = new MethodReference(new ArrayOfExpression(str),
1105:                        new ProgramElementName("append"), buffer);
1106:                body[3] = new Return(result);
1107:
1108:                ExtList args = getArguments(t);
1109:                args.add(buffer);
1110:                LinkedList params = getParameterDeclarations(args);
1111:
1112:                MethodDeclaration md = buildMethodDeclaration(body,
1113:                        new TypeRef(b), "quantifierTerm", params);
1114:                children.add(md);
1115:                return new MethodReference(args, new ProgramElementName(md
1116:                        .getName()), testTypeRef);
1117:            }
1118:
1119:            /**
1120:             * Returns the program variables occuring in t that are no atributes.
1121:             */
1122:            private ExtList getArguments(Term t) {
1123:                SetOfProgramVariable programVars = SetAsListOfProgramVariable.EMPTY_SET;
1124:                TermProgramVariableCollector pvColl = new TermProgramVariableCollector();
1125:                t.execPreOrder(pvColl);
1126:                Iterator itp = pvColl.result().iterator();
1127:                while (itp.hasNext()) {
1128:                    ProgramVariable v = (ProgramVariable) itp.next();
1129:                    if (!v.isMember()) {
1130:                        programVars = programVars.add(v);
1131:                    }
1132:                }
1133:                programVars = removeDublicates(programVars);
1134:                IteratorOfProgramVariable it = programVars.iterator();
1135:                ExtList args = new ExtList();
1136:                while (it.hasNext()) {
1137:                    args.add(it.next());
1138:                }
1139:                return args;
1140:            }
1141:
1142:            private LinkedList getParameterDeclarations(ExtList l) {
1143:                LinkedList params = new LinkedList();
1144:                Iterator it = l.iterator();
1145:                while (it.hasNext()) {
1146:                    ProgramVariable arg = (ProgramVariable) it.next();
1147:                    params.add(new ParameterDeclaration(new Modifier[0],
1148:                            new TypeRef(arg.getKeYJavaType()),
1149:                            new VariableSpecification(arg), false));
1150:                }
1151:                return params;
1152:            }
1153:
1154:            /**
1155:             * Trys to extract bounds for the quantified integer variable.
1156:             */
1157:            private void getBound(Term t, Expression[] bounds,
1158:                    ProgramVariable pv, ProgramVariable buffer, ExtList children) {
1159:                int ex = 0, less = 1;
1160:                if ((t.op().name().toString().equals("!") || t.op().name()
1161:                        .toString().equals("not"))
1162:                        && t.sub(0).op().name().toString().equals("lt")) {
1163:                    t = t.sub(0);
1164:                    less = 0;
1165:                } else if (t.op().name().toString().equals("lt")) {
1166:                    ex = 1;
1167:                } else if (t.op().name().toString().equals("leq")) {
1168:                } else if (t.op().name().toString().equals("geq")) {
1169:                    less = 0;
1170:                } else if (t.op().name().toString().equals("gt")) {
1171:                    ex = 1;
1172:                    less = 0;
1173:                } else {
1174:                    throw new NotTranslatableException("bound " + t
1175:                            + " for quantified variable");
1176:                }
1177:                if (t.sub(0).op() == pv) {
1178:                    bounds[2 * less + ex] = translateTerm(t.sub(1), buffer,
1179:                            children);
1180:                } else if (t.sub(1).op() == pv) {
1181:                    bounds[2 - 2 * less + ex] = translateTerm(t.sub(0), buffer,
1182:                            children);
1183:                } else {
1184:                    throw new NotTranslatableException("bound " + t
1185:                            + " for quantified variable");
1186:                }
1187:            }
1188:
1189:            /**
1190:             * replaces all occurences of lv in t with pv.
1191:             */
1192:            private Term replaceLogicVariable(Term t, LogicVariable lv,
1193:                    ProgramVariable pv) {
1194:                TermFactory tf = TermFactory.DEFAULT;
1195:                Term result = null;
1196:                if (t.op() == lv) {
1197:                    return tf.createVariableTerm(pv);
1198:                } else {
1199:                    Term subTerms[] = new Term[t.arity()];
1200:                    ArrayOfQuantifiableVariable[] quantVars = new ArrayOfQuantifiableVariable[t
1201:                            .arity()];
1202:                    for (int i = 0; i < t.arity(); i++) {
1203:                        quantVars[i] = t.varsBoundHere(i);
1204:                        subTerms[i] = replaceLogicVariable(t.sub(i), lv, pv);
1205:                    }
1206:                    JavaBlock jb = t.javaBlock();
1207:                    result = tf.createTerm(t.op(), subTerms, quantVars, jb);
1208:                }
1209:                return result;
1210:            }
1211:
1212:            /**
1213:             * Converts <code>t</code> to a ProgramElement. If <code>t</code> is
1214:             * a (skolem)constant, a new identically named ProgramVariable of the
1215:             * same sort is returned.
1216:             */
1217:            public Expression convertToProgramElement(Term t) {
1218:                t = replaceConstants(t, serv, null);
1219:                return serv.getTypeConverter().convertToProgramElement(t);
1220:            }
1221:
1222:            /**
1223:             * Replaces rigid constants by program variables.
1224:             */
1225:            protected static Term replaceConstants(Term t, Services serv,
1226:                    Namespace newPVs) {
1227:                TermFactory tf = TermFactory.DEFAULT;
1228:                Term result = null;
1229:                if (t.op() instanceof  RigidFunction && t.arity() == 0
1230:                        && !"#".equals(t.op().name().toString())
1231:                        && !"TRUE".equals(t.op().name().toString())
1232:                        && !"FALSE".equals(t.op().name().toString())
1233:                        && t.op() != Op.NULL) {
1234:                    KeYJavaType kjt = serv.getJavaInfo().getKeYJavaType(
1235:                            t.sort().toString());
1236:                    if (t.sort().toString().startsWith("jint")) {
1237:                        kjt = serv.getJavaInfo().getKeYJavaType(
1238:                                t.sort().toString().substring(1));
1239:                    }
1240:                    ProgramVariable pv = new LocationVariable(
1241:                            new ProgramElementName(t.op().name().toString()),
1242:                            kjt);
1243:                    if (newPVs != null) {
1244:                        newPVs.add(pv);
1245:                    }
1246:                    return tf.createVariableTerm(pv);
1247:                } else if (t.op() instanceof  ProgramVariable) {
1248:                    if (newPVs != null
1249:                            && !((ProgramVariable) t.op()).isStatic()) {
1250:                        newPVs.add((ProgramVariable) t.op());
1251:                    }
1252:                    return t;
1253:                } else {
1254:                    Term subTerms[] = new Term[t.arity()];
1255:                    ArrayOfQuantifiableVariable[] quantVars = new ArrayOfQuantifiableVariable[t
1256:                            .arity()];
1257:                    for (int i = 0; i < t.arity(); i++) {
1258:                        quantVars[i] = t.varsBoundHere(i);
1259:                        subTerms[i] = replaceConstants(t.sub(i), serv, newPVs);
1260:                    }
1261:                    JavaBlock jb = t.javaBlock();
1262:                    result = tf.createTerm(t.op(), subTerms, quantVars, jb);
1263:                }
1264:                return result;
1265:            }
1266:
1267:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.