Modularisation Plug-in Release Notes

Fixed the problem with having multiple operation postconditions constraining the same primed variable
Parallel assignment due a duplicate call is now handled gracefully
New static checker rule to ensure that implementation events are either convergent or anticipated
"Entry" flag in implementation is now called "final"
Witnesses for operation parameters may now be used in an implementation machine. It is working but not very refined: once "final" flag is set on an event and machine is saved, a refinement clause appears in the event. It is a generated element that in future platform version would not be alterable. Normally,a machine would have to be touched and saved again for any existing problems related to witnesses to disappear.

Fixed a vicious bug that may lead to infinite loop in static checker.
Fixed bug in operation precondition POG that prevented generation of POs for operations with parameters.
Added operation invariant satisfaction PO.
Added interface pretty printer.

Dealing with refinement:

The "Refine" command available from a pop-up menu of the project explorer construct an initial refinement machine that does not declare the variables imported from modules. This typically results in a number of error messages saying that a variable is not declared. The problem is solved by adding the missing declarations manually.

General:

Many necessary static checks are not implemented. It means that it is possible to run into troubles without getting any hint on what is happening. Some such checks are planned and many more are still to be discovered.
Machine pretty printer is not aware of the extensions contributed by the plugin. Thus, all the additional elements, accessible in the composite editor, do not show up at all during pretty printing.
The same problem as the above for the text editor.
The plug-in cannot work alongside any other plug-in contributing SC and POG modules. It will try to override the current configuration of a component whenever a plug-in specific model element is updated.
Interface change is not automatically reacted upon by components depending on it - there is no proper dependency link. This is particularly problematic when cleaning and rebuilding a project.

Interface components:

There is a bug in showing interface proof obligations - these are not refreshed automtically in the project explorer. To refresh the view, change a model part and save the model (e.g., type a comment)
Interface variables do not have an initialisation. This results in a warning by a SC that cannot be addressed by a user.
Currently, postconditions must be written in such a way that no two postconditions mention the same primed variable. The violation of this rule would result in a broken statically checked interface component.
Operations without return variables are not supported. This is related to the fact that, for now, an operation call is always an expression rather than a predicate or a complete action.
There is no interface pretty-printer.

Implementation machines:

It is not checked yet that all the interface operations are implemented.
No proof obligations are generated to ensure deadlock freeness of event groups realising interface operations.

Interface import:

There is no support for instantiation of given sets in imported interfaces. Set instantiation could be used to configure generic components to specific data types (or typing expressions) used in a main model.
New axioms (under the PROPERTIES section of USES) added while importing an interface are not validated in any manner except type checking.
Operation call precondition proof obligation does not select the relevant hypothesis. Also, its hypothesis include event action hypothesis that should not be the cases for the obligation.

Navigation menu