Information Technology Reference
In-Depth Information
primrec
cpList:: Component
⇒
Component list
and
cpListlist:: Component list
⇒
Component list
where
cpList (Primitive N itfs s) = [(Primitive N itfs s)] |
cpList (Composite N itfs subCp bindings s) =
(Composite N itfs subCp bindings s)#(cpListlist subCp) |
cpListlist [] = [] |
cpListlist (C#CL) = (cpList C)@ cpListlist CL
CpSet: gives a set representation of the
cpList
of a component. This allows us
to write properties in a much more intuitive way, for example, quantifying over
sub-components is easily written as
∀
∈
CpSet(C)
. Note however that a few
proofs require to stick to the
CpList
notation; indeed when switching to cpSet
construct, one cannot reason on the coexistence of two identical components.
C'
constdefs
:: Component
⇒
Component set
cpSet C == set (cpList C)
getCp: allows for retrieving a given component from a component list based on
the component Name. The constructors
Some
and
None
represent the so-called
option
datatype enabling specifications of partial functions. Here, a component
with the given name might not be defined in the list - this is nicely and eciently
modelled by a case distinction over the option type. Note the definition of
^
as
an infix operator synonymous for
getCp
. This so-called pretty printing syntax
of Isabelle supports natural notation of the form
CL^N = Some C'
.
primrec
getCp:: Component list
⇒
Name
⇒
Component option
where
getCp [] N' = None |
getCp (C#CL) N' =
if
(getName C=N')
then
Some C
else
(CL^N')
changeCp CL C: written
CL<-C
replaces the component in the list
CL
that has
the same name as
C
by
C
; it does nothing if there is no component with the given
name.
primrec
changeCp::Component list
⇒
Component
⇒
Component list
where
changeCp [] C = [] |
changeCp (C#CL) C' =
if
getName C=getName C'
then
C'#CL
else
C#(CL<-C')
removeSubCp C N: removes the subcomponent of
C
with name
N
but does
nothing if there is no subcomponent with this name. Note, here the use of a
case
switch supporting again pattern matching in Isabelle/HOL definitions.
primrec
removeSubCp:: Component
⇒
Name
⇒
Component
where
removeSubCp (Primitive N itf s) N' = (Primitive N itf s) |
removeSubCp (Composite N itf sub b s) N' = (
case
sub^N'
of
None => (Composite N itf sub b s) |
Some C => Composite N itf (remove1 C sub) b s)
Similar operations are needed for dealing with requests and results. This includes
operations for building lists of all referenced requests inside a component (and
