Information Technology Reference
In-Depth Information
a map can only serve one level. As we want component names to be unique
globally, a condition on name uniqueness is necessary.
Subcomponents are defined as lists rather than finite sets because lists come
with a convenient inductive reasoning easing proofs involving component struc-
ture. Of course it is easy to define an equivalence relation to identify components
modulo reordering. On the contrary the bindings of a component are defined as
a set because no inductive reasoning is necessary on bindings, and sets fit better
to the representation of this construct.
Having a formalisation of component structure alone, although useful, is not
sucient. An adequate infrastructure needs to be developed to help in reasoning
on the component model. The next section describes some of the infrastructure
operations that allow us to manipulate components inside component hierarchies.
3.2
Ecient Specification of Component Manipulation
This section provides various operations that allow us to effectively manipulate
components. These include operation for accessing component fields, mecha-
nisms for traversing component hierarchies, and means for replacing and up-
dating components inside the hierarchical structure. All these operations are
primitive recursive functions enabling an encoding in Isabelle/HOL using the
primrec
feature. Using this feature has great advantages for the automation of
the interactive reasoning process. Automated proof procedures of Isabelle/HOL,
like the simplifier, are automatically adapted to the new equations such that
simple cases can be solved automatically. Moreover, the definitions themselves
can use pattern matching leading to readable definitions.
Field access.
We define a number of operations for accessing various fields. These
include the function getName that returns the
Name
of the component.
primrec
getName:: Component
⇒
Name
where
getName (Primitive N itf s) = N |
getName (Composite N itf sub b s) = N
Similarly, we define
getItfs
,
getQueue
,and
getComputedResults
for getting
interfaces, request queues and replies. Requests and replies are part of the com-
ponent state described in Section 3.3.
Accessing component hierarchy.
In order to support hierarchical components,
we need a number of mechanisms to access components inside hierarchies. These
range from simply finding a suitable component inside a component list to up-
dating the relevant component with another component. The most useful of
these operations are detailed below.
cpList: returns a list of all subcomponents of a component recursively. It uses
the predefined Isabelle/HOL list operators
#
for constructing lists and
@
for
appending two lists. Note that the following primitive recursive function is mu-
tually recursive and needs an auxiliary operation dealing with component lists.
