Information Technology Reference
In-Depth Information
solution. This implies that for each atomic polynomial formula
φ
in
η
(
l
0
)
,
Θ ∧¬φ
has no real solution. Note that
η
(
l
0
)
is the conjunction of a set of
atomic polynomials and
Θ ∧¬φ
is a PSAS according to the definition. Thus,
applying the tool DISCOVERER to the resulted PSAS
Θ ∧¬φ
, we get a nec-
essary and sucient condition of the derived PSAS having no real solution.
The condition may contain the occurrences of some program variables. In
this case, the condition should hold for any instantiations of these variables.
Thus, by introducing universal quantifications of these variables (we usually
add a scope to each of these variables according to different situations) and
then applying QEPCAD, we can get a necessary and sucient condition
only on the presumed parameters.
Repeatedly apply the procedure to each atomic polynomial formula of the
predefined invariant at
l
0
and then collect all the resulted conditions.
Example 6.
In Example 5,
Θ |
=
η
1
(
l
0
)
is equivalent to
x
=0
,y
=0
,eq
(
x, y
)
=0
(5)
has no real solution. By calling
tofind
(([
x, y
]
,
[]
,
[]
,
[
eq
(
x, y
)]
,
[
x, y
]
,
[
a
1
,a
2
,a
3
,a
4
]
,
0)
we get that (5) has no real solution iff
true
.
Similarly,
Θ |
=
η
2
(
l
0
)
is equivalent to
x
=0
,y
=0
,ineq
(
x, y
)
≤
0
(6)
has no real solution. Calling
tofind
([
x, y
]
,
[
−ineq
(
x, y
)]
,
[]
,
[]
,
[
x, y
]
,
[
b
1
,b
2
,b
3
,b
4
]
,
0)
we get that (6) has no real solution iff
b
4
>
0
.
(7)
Deriving PSASs from Consecutive Condition and Solving.
From Defi-
nition 5, for each transition
τ
=
l
i
,l
j
,ρ
τ
,θ
τ
,
η
(
l
i
)
∧ ρ
τ
∧ θ
τ
|
=
η
(
l
j
)
so
η
(
l
i
)
∧ ρ
τ
∧ θ
τ
∧¬η
(
l
j
)
has no real solution. This implies that for each
atomic polynomial formula
φ
η
(
l
i
)
∧ ρ
τ
∧ θ
τ
∧¬φ
(8)
has no real solution. It is easy to see that (8) is a PSAS according to De-
finition 1, so applying the tool DISCOVERER, we obtain a necessary and
sucient condition on the parameters such that (8) has no real solution.
Subsequently, similarly to Step 2, we may need to exploit the quantifier
elimination tool QEPCAD to reduce the resulted condition in order to get
a necessary and sucient condition only on the presumed parameters.
Search WWH ::
Custom Search