Information Technology Reference
In-Depth Information
It follows that, for scalar testing it makes no difference whether convex closure is
employed or not. Therefore, vector-based testing is also a conservative extension of
scalar testing without employing convex closure.
Corollary 5.1
Suppose ʩ is the singleton set
{
ˉ
}
. Then
ʩ
1. P
pmay
Q if and only if P
pmay
Q.
pmust
Q if and only if P
pmust
Q.
2. P
Proof
The result follows from Lemma
5.1
.
Lemma
5.1
does not generalise to [0, 1]
ʩ
, when
|
ʩ
|
>
1, as the following example
demonstrates:
Example 5.1
Let
X
,
Y
denote
{
(0
.
5, 0
.
5)
}
and
{
(1, 0), (0, 1)
}
respectively. Then it
is easy to show that
≤
Ho
Y
.
This example can be exploited to show that for vector-based testing it
does
make a
difference whether convex closure is employed.
X
≤
Ho
Y
, although obviously
X
Example 5.2
Consider the two processes
P
:
=
a
2
↕
b
and
Q
:
=
a
b.
Take
ʩ
={
ˉ
1
,
ˉ
2
}
. Employing a results-gathering function without convex closure,
with the test
T
:
=
a.ˉ
1
b.ˉ
2
we would obtain
A
(
T
,
P
)
={
(0
.
5, 0
.
5)
}
A
(
T
,
Q
)
={
(1, 0), (0, 1)
}
.
As pointed out in Example
5.1
, this entails
A
(
T
,
P
)
≤
Ho
A
(
T
,
Q
), although their
convex closures
are
related under the Hoare preorder.
Convex closure is a uniform way of ensuring that internal choice can simulate an
arbitrary probabilistic choice. For the processes
P
and
Q
of Example
5.2
we will see
later on that
P
pmay
Q
. This fits with the intuition that a probabilistic
choice is an acceptable implementation of a nondeterministic choice occurring in
a specification. Considering that we use
S
Q
and
P
pmay
as a stepping stone in showing the
pmay
Q
. For this reason we used
coincidence of
S
and
pmay
, we must have
P
convex closure in Definition 4.3.
5.3
Counterexamples
We will see in this section that many of the standard testing axioms are not valid
in the presence of probabilistic choice. We also provide counterexamples for a few
distributive laws involving probabilistic choice that might appear plausible at first
sight. In all cases we establish a statement
P
pmay
Q
by exhibiting a test
T
such that
max
(
A
(
T
,
P
))
=
max
(
A
(
T
,
Q
)) and a statement
P
pmust
Q
by exhibiting a test
T
Search WWH ::
Custom Search