Information Technology Reference
In-Depth Information
its subcomponents), finding a result for a given future inside a component hier-
archy, etc. In all we provide almost 30 functions and predicates to help express
structured component specifications eciently.
Design decisions.
It is crucial for the reasoning process whether one chooses
lists or sets to represent various parts of the specified component structure. As
we have seen above the basic infrastructure we have built up to handle our
hierarchical components is mainly based on lists. Consequently, we can define
operations over components and their constituents by primitive recursion and
thereby decisively improve automated support. However, sets come with a more
natural notation. Often set theoretic properties can be simply decided by boolean
reasoning that poses no problems for logical decision procedures integrated in
Isabelle/HOL, and Isabelle/HOL comes with numerous lemmas for reasoning
on sets. On the other side, inductive reasoning on finite sets is less convenient
than on lists. In places where we want to combine the merits of both worlds, the
CpSet
function provides a convenient translation.
3.3
Component State
Our component model shall not only allow structural reasoning on hierarchical
components but also reasoning about dynamic component state. While the pre-
ceding sections provided a good formalisation valid for any hierarchical compo-
nent model, we now define component state in order to support communication
by request and replies. Those constructs are used to define our component se-
mantics, as shown in Section 4.1. Let us first focus on the high level definition of
states which provide the constructs relating the component structure with the
dynamic semantics
2
. We show below the two types of component states (for com-
posite and primitive components) used in the definition of
Component
presented
in Section 3.1.
record
CompState =
record
PrimState =
Cqueue:: Request list
Pqueue:: Request list
CcomputedResults:: Result list
PcomputedResults:: Result list
PintState:: intState
behaviour:: Behaviours
Each state contains a queue of pending requests, and a list of results computed by
this component. Additionally, primitive components have an internal state and
a behaviour for encoding the business logic, see below. We use the Isabelle/HOL
record
type constructor here; it automatically defines field projection as func-
tions, e.g. for a
Compstate s
,
(Cqueue s)
accesses its request queue. Note that
uniqueness of fields identifier required us to add a '
C
'or'
P
' prefix to fields of
component states to distinguish them.
The definition of the component state relies on the definitions of requests
(characterized by a future identifier, a parameter, and a target interface), and
results (characterized by the future identifier and its value).
2
The real definition of component states contains additional fields; only the fields of
interest for this paper are shown here.
