01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: package de.uka.ilkd.key.proof.init;
09:
10: /**
11: * Proof obligations resulting from the OCL Simplification implement this interface.
12: * Currently the main reason is to avoid some dependencies on Together OpenAPI which
13: * make it impossible to compile KeY without Together.
14: */
15:
16: public interface OCLSimplificationPO {
17:
18: /**
19: * Adds OCL types, OCL operations, and model properties to the
20: * name spaces of the initial configuration.
21: * Can as well be hard-coded, since they are needed for all
22: * OCL simplification. Also avoids trouble with taclet parser.
23: * @param initConf The initial configuration whose set of name
24: * spaces needs to be updated.
25: */
26: void createNamespaceSet(InitConfig initConf);
27:
28: }
|