Information Technology Reference
In-Depth Information
3.4.3
Components
From the perspective of structural organization, every component is represented in
a CSP as a set of variables (inputs, outputs, parameters) from the integer domain,
and a set of constraints, which correspond to the contracts implemented by that
component (see Figure 4). Note that we distinguish here between variables used in
Component
Variables: Inputs, Outputs, Parameters
Component Constraint C
m
Contract C1
Assumptions
Contract 1
Guarantees
Contract Constraint C
s1
Contract Part 1 C
sp1
Local A/G Variables
A/G Constraints C
agc
Composition Constraints C
cc
Binding Constraints C
bc
Refined/Alternative Contract C1'
Assumptions
Guarantees
...
Contract Part n C
pn
Contract n
...
Fig. 4
Representation of a component in CSP (left) and an excerpt of the mapping the con-
tracts to constraints and variables (right)
components, i.e.
in relation
(2). Although they are identical, we define separated variables in the CSP for each
of them. This means, when a component has two contracts, we have CSP variables
for (a) component variables (inputs, outputs and parameters) and (b) CSP variables
(inputs, outputs and parameters) for each contract. With this separation of contracts
and components, we can identify which contracts are satisfied if the verification
succeeds. As mentioned, the constraint solver not only responds with a decision,
butitalsofindsallvaluesof
X
CSP
for which the verification succeeds. Similarly, if
the verification fails, the conflicting contracts can be easily identified.
Now we describe how the contracts are defined in a CSP, how they are linked with
components, and how the criteria for correctness from relation (5) is represented in
aCSP.
Σ
in relation (4), and variables used in contracts, i.e.
Σ
3.4.4
Contracts
As shown in Figure 4, each contract is represented as a single top-level constraint
C
s
.
This constraint is further related to a set of local A/G variables (inputs, outputs, pa-
rameters) and a set of sub-constraints. The sub-constraints represent the constraints
Search WWH ::
Custom Search