A Framework for Reasoning on Component Composition - Formal Methods for Components and Objects - page 11

record Request = record Result =

id::Fid fid::Fid

parameter:: Value fValue:: Value

invokedItf:: Name

An interesting construct is the representation of component behaviour. Each
primitive component has an internal state. A behaviour specifies how a primitive
component passes from an internal state to another. It is defined as a labeled
transition system between internal states of a component:

typedef Behaviours={ beh::(intState × Action × intState) set.
( ∀ s s'. ((s,Tau,s') ∈ beh −→ (set (PRqRefs s') ⊆ set (PRqRefs s))
∧ PcurrentReqs s' = PcurrentReqs s)) ∧

...}

The type Behaviours is defined as a set of triples (internal state, action, internal
state). In our case actions are: internal transition ( Tau , shown here), request
service, request emission, result reception, and end of service which associates a
result to a request. More than the precise definition of our actions, it is interesting
to focus on the way behaviour can be defined and further refined by constraints.
Additional rules are specified to restrain the possible behaviours, preventing
incorrect transitions to occur; for example, we forbid replying to a non-existing
request. In the piece of code above we require conditions on the internal state
before and after an internal transition: the set of referenced futures can only be
smaller after an internal transition, and the set of currently served requests is
unchanged. More complex conditions are imposed for other actions.

Design decisions. Isabelle/HOL extensible records are the natural choice for
representing states, requests, and results. They are better suited than simple
products because they support qualified names implicitly. We did, however, not
use the additional extension property of records which is similar to inheritance
known from object-orientation. It could have been used to factor out the shared
parts of primitive and composite components but this is not worthwhile - prop-
erties specific to the shared parts are few. Hence, there is practically no overhead
caused by duplicating basic lemmas. The use of lists for requests and results is
important for the ecient specification and proof of structural properties (see
the design decisions in the previous section). The definition of behaviours in
the internal state of primitive components uses an Isabelle/HOL type definition.
This way, we can encapsulate the predicate defining the set of all well-formed
behaviours into a new HOL type. These constraints are thereby implicitly car-
ried over and can be re-invoked by using the internal isomorphism with the set
Behaviours .

3.4 Correct Component

We presented the structure of our components in Section 2.2, while the various
constructs designed to manipulate hierarchical components appear in Section 3.2.