| java.lang.Object
 de.uka.ilkd.key.ocl.gf.GFinterface
All known Subclasses: de.uka.ilkd.key.casetool.together.TogetherGFInterface,
| GFinterface | | abstract public class GFinterface (Code) | | control object interfacing KeY with GF.
Saves the editor from knowing, that KeY exists
|
| Method Summary | |
| public String | editClassInvariant(String classname, String pack, String ocl, CallbackClassInv cci, ProgressMonitor pm, String absFromTogether)
Starts the GF editor for OCL for editing a class invariant
Parameters:
classname - The name of the class whose invariant should be edited
Parameters:
pack - the package of the class whose invariant should be edited
Parameters:
ocl - the OCL invariant
Parameters:
cci - a special callback class, must be properly initialized
Parameters:
pm - to monitor the loading progress. | | public String | editPrePost(String classname, String pack, String opersig, String pre, String post, CallbackPrePost cpp, boolean isQuery, ProgressMonitor pm, String absFromTogether)
Start GF editor for editing pre-/postcondition of a method/operation
Parameters:
classname - the name of class of the operation
Parameters:
pack - the name of the package the class is in
Parameters:
opersig - signature of the operation
Parameters:
pre - string containg OCL precondition (currently ignored)
Parameters:
post - string containg OCL postcondition (currently ignored)
Parameters:
isQuery - if the method is a query
Parameters:
pm - to monitor the loading progress. | | public void | ocl2nlExport(File oclFile, File nlFile, String format)
|
| AUTO_GENERATE | | final static boolean AUTO_GENERATE(Code) | | |
| model | | protected UMLOCLModel model(Code) | | get's defined in subclass @see TogetherGFInterface.
|
| modelInfoUmltypes | | public String modelInfoUmltypes(Code) | | get's defined in subclass @see TogetherGFInterface.
Contains the place where modelinfo.umltypes is put
|
| modelModulName | | final public static String modelModulName(Code) | | |
| modelinfoUmltypesFilename | | final protected static String modelinfoUmltypesFilename(Code) | | |
| projectRoot | | protected String projectRoot(Code) | | path to the Together project, get's written in subclass
|
| editClassInvariant | | public String editClassInvariant(String classname, String pack, String ocl, CallbackClassInv cci, ProgressMonitor pm, String absFromTogether)(Code) | | Starts the GF editor for OCL for editing a class invariant
Parameters:
classname - The name of the class whose invariant should be edited
Parameters:
pack - the package of the class whose invariant should be edited
Parameters:
ocl - the OCL invariant
Parameters:
cci - a special callback class, must be properly initialized
Parameters:
pm - to monitor the loading progress. May be null
Parameters:
absFromTogether - The abstract syntax tree saved as a JavaDoc from previous runs message to Together (only if something went wrong?) |
| editPrePost | | public String editPrePost(String classname, String pack, String opersig, String pre, String post, CallbackPrePost cpp, boolean isQuery, ProgressMonitor pm, String absFromTogether)(Code) | | Start GF editor for editing pre-/postcondition of a method/operation
Parameters:
classname - the name of class of the operation
Parameters:
pack - the name of the package the class is in
Parameters:
opersig - signature of the operation
Parameters:
pre - string containg OCL precondition (currently ignored)
Parameters:
post - string containg OCL postcondition (currently ignored)
Parameters:
isQuery - if the method is a query
Parameters:
pm - to monitor the loading progress. May be null
Parameters:
absFromTogether - The abstract syntax tree saved as a JavaDoc from previous runs message to Together (if something went wrong) |
| ocl2nlExport | | public void ocl2nlExport(File oclFile, File nlFile, String format)(Code) | | translate all OCL specs in a text file to NL
Parameters:
format - should be either "html" or "latex" |
|
|