Difference between revisions of "Modularisation Plug-in"

From Event-B
Jump to navigationJump to search
imported>Alexei
(New page: 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 ver...)
 
imported>Alexei
Line 35: Line 35:
 
  post3  :  size' = top + 1
 
  post3  :  size' = top + 1
 
    END
 
    END
 
 
pop  ≙  PRE
 
pop  ≙  PRE
pre1  :  top > 0
+
pre1  :  top > 0
 
    RETURN
 
    RETURN
 
  value
 
  value

Revision as of 23:25, 9 October 2009

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.


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.

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