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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.speclang.ocl;
019:
020: import java.io.StringReader;
021: import java.util.Map;
022:
023: import antlr.ANTLRException;
024:
025: import de.uka.ilkd.key.java.Services;
026: import de.uka.ilkd.key.logic.EverythingLocationDescriptor;
027: import de.uka.ilkd.key.logic.ListOfInteger;
028: import de.uka.ilkd.key.logic.NamespaceSet;
029: import de.uka.ilkd.key.logic.SLListOfInteger;
030: import de.uka.ilkd.key.logic.SetAsListOfLocationDescriptor;
031: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
032: import de.uka.ilkd.key.logic.Term;
033: import de.uka.ilkd.key.logic.TermBuilder;
034: import de.uka.ilkd.key.logic.TermFactory;
035: import de.uka.ilkd.key.logic.op.IteratorOfParsableVariable;
036: import de.uka.ilkd.key.logic.op.ListOfParsableVariable;
037: import de.uka.ilkd.key.logic.op.LogicVariable;
038: import de.uka.ilkd.key.logic.op.ParsableVariable;
039: import de.uka.ilkd.key.logic.op.ProgramVariable;
040: import de.uka.ilkd.key.parser.KeYLexer;
041: import de.uka.ilkd.key.parser.KeYParser;
042: import de.uka.ilkd.key.parser.ParserMode;
043: import de.uka.ilkd.key.parser.ocl.AxiomCollector;
044: import de.uka.ilkd.key.parser.ocl.FunctionFactory;
045: import de.uka.ilkd.key.parser.ocl.KeYOclLexer;
046: import de.uka.ilkd.key.parser.ocl.KeYOclParser;
047: import de.uka.ilkd.key.parser.ocl.OCLTranslationError;
048: import de.uka.ilkd.key.speclang.FormulaWithAxioms;
049: import de.uka.ilkd.key.speclang.SLTranslationError;
050: import de.uka.ilkd.key.util.Debug;
051:
052: /**
053: * Translates OCL expressions to DL.
054: */
055: public class OCLTranslator {
056: private final Services services;
057: private ListOfInteger parserCounters = SLListOfInteger.EMPTY_LIST;
058:
059: public OCLTranslator(Services services) {
060: this .services = services;
061: }
062:
063: private FormulaWithAxioms translatePrePostInv(String expr,
064: ParsableVariable selfVar, ListOfParsableVariable paramVars,
065: ParsableVariable resultVar, ParsableVariable excVar)
066: throws SLTranslationError {
067: AxiomCollector ac = new AxiomCollector();
068: FunctionFactory.INSTANCE.resetFactory(services, ac);
069:
070: Term resultFormula = null;
071: Map resultAxioms = null;
072:
073: try {
074: //create lexer and parser
075: StringReader stream = new StringReader(expr);
076: KeYOclLexer lexer = new KeYOclLexer(stream);
077: KeYOclParser parser = new KeYOclParser(lexer, services, ac,
078: selfVar, paramVars, resultVar, excVar);
079:
080: //initialise counters
081: parser.setCounters(parserCounters);
082:
083: //parse the expression
084: if (expr.length() > 0) {
085: resultFormula = parser.parseExpression();
086: } else {
087: resultFormula = TermBuilder.DF.tt();
088: }
089:
090: //get created Axioms
091: resultAxioms = ac.getAxioms();
092:
093: //save counter values
094: parserCounters = parser.getCounters();
095: } catch (ANTLRException e) {
096: if (e instanceof OCLTranslationError) {
097: throw ((OCLTranslationError) e).getSLTranslationError();
098: } else {
099: Debug.fail("OCLTranslator : " + e.getMessage());
100: }
101: }
102: return new FormulaWithAxioms(resultFormula, resultAxioms);
103: }
104:
105: public FormulaWithAxioms translatePre(String pre,
106: ParsableVariable selfVar, ListOfParsableVariable paramVars)
107: throws SLTranslationError {
108: return translatePrePostInv(pre, selfVar, paramVars, null, null);
109: }
110:
111: public FormulaWithAxioms translatePost(String post,
112: ParsableVariable selfVar, ListOfParsableVariable paramVars,
113: ParsableVariable resultVar, ParsableVariable exceptionVar)
114: throws SLTranslationError {
115: return translatePrePostInv(post, selfVar, paramVars, resultVar,
116: exceptionVar);
117: }
118:
119: public SetOfLocationDescriptor translateModifies(String modifies,
120: ParsableVariable selfVar, ListOfParsableVariable paramVars)
121: throws SLTranslationError {
122: if (modifies == null || modifies.equals("")) {
123: return SetAsListOfLocationDescriptor.EMPTY_SET
124: .add(EverythingLocationDescriptor.INSTANCE);
125: }
126:
127: NamespaceSet nss = services.getNamespaces().copy();
128: IteratorOfParsableVariable it = paramVars.prepend(selfVar)
129: .iterator();
130: while (it.hasNext()) {
131: ParsableVariable pv = it.next();
132: if (pv instanceof LogicVariable) {
133: nss.variables().add(pv);
134: } else {
135: assert pv instanceof ProgramVariable;
136: nss.programVariables().add(pv);
137: }
138: }
139:
140: try {
141: KeYParser parser = new KeYParser(ParserMode.TERM,
142: new KeYLexer(new StringReader(modifies), null), "",
143: TermFactory.DEFAULT, services, nss);
144: return parser.location_list();
145: } catch (Exception e) {
146: throw new SLTranslationError(e.getMessage(), 0, 0);
147: }
148: }
149:
150: public FormulaWithAxioms translateInv(String inv,
151: ParsableVariable selfVar) throws SLTranslationError {
152: return translatePrePostInv(inv, selfVar, null, null, null);
153: }
154: }
|