Generating Polynomial Invariants with DISCOVERER and QEPCAD - Formal Methods and Hybrid Real-Time Systems - page 76

these parameters and therefore get an invariant for each underlining location by
replacing with the resulted instantiations the parameters of the predetermined
parametric PSAS. The above procedure are supported by the computer algebra
tools DISCOVERER and QEPCAD.
We will use the following example to demonstrate our approach in details.

Example 5. Consider a program shown in Fig.1 (a).

P = V = {x, y}
L = {l 0 }
T = {τ }}
where
τ = l 0 ,l 0 ,x − x − y 2 =0 ∧ y − y − 1=0 ,
x ≥ 0 ∧ y ≥ 0

Integer ( x, y ):=(0 , 0);
l 0 : while x ≥ 0 ∧ y ≥ 0 do
( x, y ):=( x + y 2 ,y +1);

end while

(a) (b)

Fig. 1.

Thus, the corresponding SATS can be represented as in Fig.1 (b).

In the following, we concretize the above idea and demonstrate with the toy
example.

Predefining Invariant. Predetermine a template of invariants at each of the
underlining location, which is a PSAS, i.e. the conjunction of a set of atomic
polynomial formula. All of these predefined PSASs form a parametric invari-
ant of the program. For example, we can assume a template of invariants of
P at l 0 in Example 5 as

eq ( x, y )= a 1 y 3 + a 2 y 2 + a 3 x − a 4 y =0 (3)

ineq ( x, y )= b 1 x + b 2 y 2 + b 3 y + b 4 > 0 ,

(4)

where a 1 ,a 2 ,a 3 ,a 4 ,b 1 ,b 2 ,b 3 ,b 4 are parameters. Therefore, η ( l 0 )=(3) ∧ (4) .
Note that theoretically speaking we can predefine a PSAS as an invariant at
each location like in the above example, but this will raise the complexity
dramatically as thus the number of parameters is so large (the reader will
see this point from the complexity analysis in the later). In practice, alter-
natively, we will split a complicated invariant to several simple invariants
such that the image of every of these simple invariants at each location is
just one of the atomic subformulae of the image of the complicated invariant
at the location. For example, in the above example, we can split η to η 1 and
η 2 by letting η 1 ( l 0 )=(3) and η 2 ( l 0 )=(4) . It is easy to prove that a program
has a complicated invariant iff the corresponding simple invariant exist, for
instance, η exists iff η 1 and η 2 exist. This is because every invariant of a
program is determined by the program itself.
Deriving PSASs from Initial Condition and Solving. Accordingtothe
initial condition in Definition 5, we have Θ | = η ( l 0 ) which means that each
real solution of Θ must satisfy η ( l 0 ) .Inotherwords, Θ ∧¬η ( l 0 ) has no real