Information Technology Reference
In-Depth Information
Example 8.
From Examples 6 & 7, it follows the necessary and sucient con-
dition on the parameters of
η
1
is (13). By using DISCOVERER, we get an
instantiation
(
a
1
,a
2
,a
3
,a
4
)=(
−
2
,
3
,
6
,
1)
.
Thus,
η
1
(
l
0
)=
−
2
y
3
+3
y
2
+6
x − y
=0
. Also, the necessary and sucient condi-
tion on the parameters of
η
2
is
(7)
∧
(17)
. By PCAD of DISCOVERER, it results
the following instantiation
(
b
1
,b
2
,b
3
,b
4
)=(1
, −
1
,
2
,
1)
that is,
η
2
(
l
0
)=
x − y
2
+2
y
+1
>
0
. Totally, we get the following invariant for the
program
P
:
−
2
y
3
+3
y
2
+6
x − y
=0
,
x − y
2
+2
y
+1
>
0
Note that the above procedure is
complete
in the sense that for any given pre-
defined parametric invariant, the procedure can always give you an answer, yes
or no. Therefore, we can conclude that our approach is also
complete
in the
sense that once the given polynomial program has a polynomial invariant, our
approach can indeed find it theoretically. This is because we can assume para-
metric invariants in program variables of different degrees, and repeatedly apply
the above procedure until we obtain a polynomial invariant.
5
Complexity Analysis
Assume given an SATS
P
=
V, L, T, l
0
,Θ
, applying the above procedure, we
obtain
k
distinct PSASs so that the predefined parametric invariants form an
invariant of the program iff none of these
k
PSASs has any real solution. W.l.o.g.,
suppose each of these
k
PSASs has at most
s
polynomial equations, and
m
in-
equations and inequalities. All polynomials are in
n
indeterminates (i.e., variables
and parameters) and of degrees at most
d
.
For a PSAS
S
,by[3],CAD(
cylindrical algebraic decomposition
) based quan-
tifier elimination on
S
has complexity
O
((2
d
)
2
2
n
+8
(
s
+
m
)
2
n
+6
)
, which is double
exponential w.r.t.
n
. Thus, the total cost is
O
(
k
(2
d
)
2
2
n
+8
(
s
+
m
)
2
n
+6
)
for directly
applying the technique of quantifier elimination to generate an invariant of a
program as advocated by Kapur [17].
In contrast, the cost of our approach includes two parts: one is for apply-
ing real solution classification to generate condition on the parameters possibly
together with some program variables; the other is for applying first-order quan-
tifier elimination to produce condition only on the parameters (if necessary) and
further exploiting PCAD to obtain the instantiations of these parameters.
The first part consists of three main steps. Firstly, we transform the equa-
tions in
S
into triangular sets (i.e., equations in triangular form) by Ritt-Wu's
method. By [12], the complexity of computing the first characteristic set is
O
(
s
O
(
n
)
(
d
+1)
O
(
n
3
)
)
. Thus, the complexity of this step is
O
(
s
n
O
(1)
(
d
+1)
n
O
(1)
)
,
which is usually called a singly exponential complexity w.r.t.
n
. Secondly, we
Search WWH ::
Custom Search