Modularisation Plug-in

From Event-B
Revision as of 18:20, 12 October 2009 by imported>Alexili
Jump to navigationJump to search

Return to Rodin Plug-ins


The Modularisation plug-in provides facilities for structuring Event-B developments into logical units of modelling, called modules. The module concept is very close to the notion Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module comes with an interface. An interface defines the conditions on how a module may be incorporated into another development (that is, another module). The plug-in follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.

Provisional Plug-in Logo

Please see the Modularisation Plug-in Installation Instructions for details on obtaining and installing the plug-in.

Module Interface

An interface is a new type of Rodin component. It similar to machine except it may not define events but rather defines one a more operations. Like a machine, an interface may import contexts, declare variables and invariants.

An operation definition is made of the following parts:

  • Label - this defines an operation name so that it can be referred by another module;
  • Parameters - a vector of (formal) operation parameters;
  • Preconditions - a list of predicates defining the states when an operation may be invoked. It is checked that caller always respects these conditions. Like event guards, preconditions also type and constrain operation parameters;
  • Return variables - a vector of identifiers used to provide a compound operation return value;
  • Postconditions - a list of predicates defining the effect of an operation on interface variables and operation return variables. Like event actions, these must maintain an interface invariant.
Interface Editor

An interface has no initialisation event. It is an obligation of an importing module to provide a suitable initial state.

The following is an example of a very simple interface describing a stack module. It has two variables - the stack top pointer and stack itself, and two operations: push and pop.


INTERFACE stack
VARIABLES top, stack
INVARIANTS
	inv1   :   	top ∈ ℕ
	inv2   :   	stack ∈ 0‥top−1 → ℕ
OPERATIONS
	push   ≙  ANY value PRE
			pre1   :   	value ∈ ℕ
		  RETURN
			size
		  POST
			post1   :   	top' = top + 1
			post2   :   	stack' = stack ∪ {top ↦ value}
			post3   :   	size' = top + 1
		  END
	pop   ≙   PRE
			pre1   :   	top > 0	
		  RETURN
			value
		  POST
			post1   :   	value' = stack(top − 1)
			post2   :   	top' = top − 1
			post3   :   	stack' = {top−1} ⩤ stack
		  END
END


The interface editor is based on the platform composite editor and follows the same principles and structure.

Importing a Module

To benefit from the services provided by a module one imports a module into a machine. The plug-in provides machine syntax extension for importing modules into a machine.

USES 
	prefix1 : 		module1
	prefix2 :		module2
	...

Prefix is a string literal used to emulate a dedicated namespace for each module. It has the effect of changing the names of all the imported elements by attaching the specified prefix string. The second parameters of Uses is a name of an interface component.

To import a module one has to know its interface. Only arriving at the implementation stage one cares to collect all the relevant module implementations and assemble them into a single system. During the modelling stage, the focus is always on a particular module. Thus, several teams may work on different modules simultaneously.

Interface proof obligations in the Project Explorer

This is what happens when importing a module -

  • all the constants, given sets and axioms visible to the interface of an imported module is visible to the importing machine, although, if a module prefix is specified, constant and given set names are changed accordingly and axioms are dynamically rewritten to account for such change;
  • interface variables and invariants becomes the variables and invariants of the importing machine. The prefixing rule also applies to variables and imported invariants are rewritten to adjust to variable name changes. Technically, imported variables are new concrete variables;
  • for static checking purposes, operations appear as constant values or constant relations. These are prefixed as well also, at this stage, they are nothing more than typed identifiers;

Having added a module import to a machine, one typically proceeds by linking the state of the imported module with the state of the machine. This is done by adding new invariants relating machine and interface variables, much like adding a gluing invariant during refinement. The constants from an imported module may be used at this stage.

Imported interface variables may be used in invariants, guards and action expressions. They may not, however, be updated directly in event actions. The only way to change a value of an interface variable is by calling one of the interface operations.

The only place where an imported operation may appear is an action expression. Since it is a state updating relation it may not be a part of a guard or invariant.

Calling an operation

To integrate a service provided by an imported module into a main development, event actions are refined to rely on the newly available functionality of an imported module. Interface operations are added into expression with a syntax resembling a operation call:

Operation pre- and post-conditions are used to describe the operation call in a proof obligation.
x := pop
...
y := push(7)

Several operation call may be combined to form complex action expression:

z := push(pop * pop)

There no limit on the way operation calls may be composed (subject to typing and verification conditions) although proof obligation complexity could make it impractical having many nested calls. The following is an event saving number from i to 0 in a stack:

save ≙ WHEN
		grd1: i > 0
	THEN
		act1: pos ≔ push(i)
		act2: i ≔ i − 1
	END
	
	

Implementing a Module

Implementing a module is similar to constructing a refinement of a machine. The formal link between a machine and an interface is declared using the new Implements clause:

MACHINE m
IMPLEMENTS iface
  ...

Like in refinement, the variables and constants of interface are visible to an implementing machine. However, unlike module import, this time interface variables play the role of abstract variables.

An interface operation is realised by a set of events. It is required to provide a realisation (however abstract) for all the interface operations. A connection between an event and operation is established by marking an event as a part of a specific event group.


Examples

Two small-scale examples are available:

  • [[1]] - a model of queue based on two ticket machine module instantiations (very basic)
  • [[2]] - two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only)