Modules and interfaces Sample Clauses

Modules and interfaces. Rodin Platform’s modularisation plug-­‐in, described and demonstrated in [RD7], [RD10], [RD11] and [RD14], provides facilities for structuring Event-­‐B developments into logical units of modelling, called modules. The module concept is very close to the notion of classical B imports. 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.