001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.casetool.patternimplementor.patterns;
009:
010: import de.uka.ilkd.key.casetool.patternimplementor.*;
011:
012: /**
013: * Implements a simplified database query pattern. This pattern implementation is
014: * part of the tutorial "How to create my own pattern?" outlined in the KeY Book.
015: */
016: public class SimpleDatabaseQuery implements AbstractPatternImplementor {
017:
018: /** file name of the OCL template file */
019: private static final String oclTemplateFilename = "simpleDatabaseQuery.constraint";
020:
021: private PIParameterGroup paramGroup;
022: private ConstraintMechanism oclTemplate;
023:
024: /**
025: * returns the instantiated template
026: */
027: public SourceCode getImplementation() {
028:
029: final SourceCode src = new SourceCode();
030:
031: final String database = paramGroup.get("database").getValue();
032: src.beginClass(database);
033:
034: src.add("(/**");
035:
036: // get table definiton instantiations
037: final String tableName = paramGroup.get("tableIdentifier")
038: .getValue();
039: final String[] tableStructure = ((PIParameterMultiString) paramGroup
040: .get("tableStructure")).getValues();
041: final String generatorExpression = paramGroup.get(
042: "generatorExpression").getValue();
043:
044: // add definition of table
045:
046: src.add(" * @definitions ");
047:
048: StringBuffer tblDef = new StringBuffer(tableName
049: + ": Sequence(TupleType(");
050: for (int i = 0, size = tableStructure.length; i < size; i++) {
051: if (i != 0)
052: tblDef.append(", ");
053: tblDef.append(tableStructure[i]);
054:
055: }
056: tblDef.append("))");
057: tblDef.append(" = " + generatorExpression);
058: src.add(" * \t " + tblDef.toString());
059:
060: // add database query
061: src
062: .add(oclTemplate.getConstraints(" * ", "Database",
063: database));
064:
065: src.add("*/");
066: return src;
067: }
068:
069: /**
070: * creates the parameter group required for the simple database query
071: * specification pattern.
072: */
073: private void createParameters() {
074: paramGroup = new PIParameterGroup("simpleDatabaseQueryPattern",
075: "Simple Database Query Pattern");
076:
077: PIParameterString context = new PIParameterString("database",
078: "Database", "Database");
079:
080: PIParameterGroup tableDefinitionGroup = new PIParameterGroup(
081: "tableDefinition", "Table Definition");
082: tableDefinitionGroup.add(new PIParameterString(
083: "tableIdentifier", "Tablename", "table"));
084: tableDefinitionGroup.add(new PIParameterMultiString(
085: "tableStructure", "Tablestructure", "e1:T1, e2:T2"));
086: tableDefinitionGroup.add(new PIParameterString(
087: "generatorExpression", "Table generator", ""));
088:
089: /*
090: * add parameter specifying the class used as database
091: * to the pattern's parameter group
092: */
093: paramGroup.add(context);
094:
095: /* add table definition group to the pattern's parameter group */
096: paramGroup.add(tableDefinitionGroup);
097:
098: /* add query definition group to the pattern's parameter group */
099: oclTemplate = new ConstraintMechanism(oclTemplateFilename,
100: paramGroup, this );
101:
102: }
103:
104: /**
105: * returns the ParameterGroup to be filled out by the specifier
106: * @return the ParameterGroup
107: */
108: public PIParameterGroup getParameters() {
109: if (paramGroup == null) {
110: createParameters();
111: }
112: return paramGroup;
113: }
114:
115: public String getName() {
116: return "Specification Pattern:Simple Database Query Pattern";
117: }
118:
119: }
|