=Paper=
{{Paper
|id=None
|storemode=property
|title=The Static Analysis of Linear Loops
|pdfUrl=https://ceur-ws.org/Vol-1356/paper_79.pdf
|volume=Vol-1356
|dblpUrl=https://dblp.org/rec/conf/icteri/LvovT15
}}
==The Static Analysis of Linear Loops==
https://ceur-ws.org/Vol-1356/paper_79.pdf
The Static Analysis of Linear Loops
Michael Lvov1, Yulia Tarasich1,
1
Kherson State University, 40 rokiv Zhovtnya St. 27
73000, Kherson, Ukraine
{Lvov, YuTarasich}@ksu.ks.ua
Abstract. In the first part of the paper, we consider the problem of generation
of polynomial invariants of iterative loops with operator of initialization of loop
and non-singular linear operator in the loop body. In the article we also show
the algorithm for calculating the basic invariants for linear operator of the
Jordan cell, and an algorithm for calculating the basic invariants of
diagonalizable linear operator with an irreducible minimal characteristic
polynomial. The second part presents a new method for proving the invariance
of the system of linear inequalities and of termination of certain linear iterative
loops of imperative programs whose data are elements of the constructive
linearly ordered field. The theoretical material of the paper is illustrated by
examples.
Keywords. Static program analysis, polynomial invariant of a loop, invariant
system of linear inequalities, eigenpolynomial of a linear operator.
Key Terms. VerificationProcess, Method, FormalMethod
1 Introduction
As for now, methods of program statistical analysis are being studied intensely.
One of the important problems is a problem of the automatic generation of program
invariants. Invariants of program are used particularly in methods of programs
verification.
The problem of searching for loop invariants in imperative programs was offered
by R. Floyd [1] and C. Hoare [2].
A correctness property of the program is formulated in terms of its total or partial
correctness. Often, the proof of termination of the program should be implemented
separately from the proof of its partial correctness. The algorithmic unsolvability of
the termination problem shows that the general algorithm of proof of termination of
the program does not exist. To prove the partial correctness of programs, Р. Floyd and
S. Hoare offered the idea of building loop invariants [1] and invariant relations in
control points of programs [2], which allows to prove programs by method of math
induction.
Thus, there is a problem of finding the invariants of the program as a key problem
of analysis of programs properties.
Now, the main attention is paid to the problem of constructing polynomial
invariant equalities. A set of invariant equalities forms the polynomial ideal, a finite
basis of which one must build. Note that in a general case, the problem of
constructing this basis has not been solved.
The existence and efficiency of algorithms to generate program invariants depend
on the subject domain, i.e., on the properties of the data algebras the program deals
with. Problems of automatic generation of program invariants for various data
algebras have been being analyzed since beginning of 1970s at the Institute of
cybernetics of NAS of Ukraine. Their main results are represented in [3,4].
Numerical data algebras are the most important from the practical point of view.
The paper [5] outlines two methods of constructing polynomial invariant equalities
types in programs whose data algebra is the domain of integrity (polynomially
determinate programs) or a field (rationally determinate programs).
This idea used in [6] to generate polynomial invariants of bounded degree for
polynomially determined programs. Program conditions such as f ( X ) 0 were
taken into account, where f (X ) are polynomials of program variables. In [7] they
proposed a method to generate polynomial program invariants of bounded degree in
linearly determinate (affine) programs containing recursive procedure calls.
In [8] they proposed a method to generate polynomial loop invariants as template
polynomials with the use of the algorithm for computing Grobner bases. In [9] they
described a method to generate nonlinear and, generally speaking, nonpolynomial
invariant relation for linear loops. The method uses eigenvalues and eigenvectors of
the linear operator in the loop body.
The paper [10] is devoted to the algebraic fundamentals of the problem of
generating polynomial loop invariants. The main result of the study is an algorithm
for generating all polynomial invariants for loops with so-called solvable assignment
operators. In particular, affine operators with positive real eigenvalues are solvable.
The same authors [11] proposed a method to generate polynomial loop invariants,
including enclosed loops, as well as program conditions in the form of both
polynomial equalities and inequalities. The paper considers a great number of
examples and presents tables for the algorithm time depending on technical
parameters of the program being analyzed.
In [12] they proposed an algorithm to search for loop invariants based on a system
of recurrent relations with loop variables and parameter n, which is the loop index.
The algorithm searches for the solution of this system not depended on n. It is
implemented in Theorema software system and is illustrated with examples in detail.
The problem of the description of invariant inequalities is less studied. The main
intricacy lies in the infinity of the basis of the metaideal [13] of polynomial
inequalities [13, 14]. Iterative methods for solving the problem of the description of
linear invariant inequalities were considered in [15-18]. In [15], the problem of
generation of the simplest invariant inequalities is solved. In [16-17], general iterative
methods are used to solve the problem of searching for linear invariant inequalities.
In [19] they described a method of proving the invariance of the system of linear
inequalities for a class of linear iterative loops with real eigennumbers of linear
operators in the loop body. This method can be applied to the entire class of linear
iterative loops and it can also be applied to prove their termination. The paper with
description of it is under preparation for a publication.
2 The Static Analysis of Polynomial Invariant Equations
2.1 L-invariants of Linear Maps and Invariants of Linear Loops.
Definition 1. Let W be an n-dimensional vector space over the field of rational
_
numbers Q and let Q be the algebraic closure of the field Q . Let X ( x1 ,....xn )
_
be an n -dimensional vector of variables. A rational function p( X ) Q( X ) is
called L-invariant of a linear operator A : W W if, for any vector b W the
following relationship holds:
p( A b) p(b) (1)
Example 1. (a linear operator with characteristic polynomial x 2 )
3
Let us consider a linear operator with the matrix
0 1 0
A 0 0 1 , X ( x, y, z ) .
2 0 0
It's easy to calculate [26], that the rational expression
(12 x 1 y z )(32 x 3 y z )
p( x, y, z ) (2)
(22 x 2 y z ) 2
2 2
where 1 2 , 2 2 , 3 2 , and cos( ) i sin( ) is the
3 3 3 2
3 3
primitive third root of unity, is the L-invariant of this operator.
Definition 2. Let X ( x1 ,..., xn ) and b (b1 ,..., bn ) - be two collections of
variables. The following fragment of an imperative program is called a linear loop:
X := b;
While Q(X, b) do X := A*X
Remark 1. Operators X:=b and X:=A*X are interpreted as simultaneous
assignments of the values of the variables of the right sides to the variables on the left
sides. In what follows, we ignore the condition Q(X, b) and consider that the linear
loop is infinite and that its execution is nondeterministic. Thus, we consider loops of
the form
X := b;
While True|False do X := A*X (3)
Definition 3. Let a vector b( 0) (b1( 0) ,..., bn( 0) ) W be chosen as initial.
( j 1)
Sequence of vectors, set by recurrent correlation b Ab , will be called the
( j)
orbit of linear operator A .
A loop sets the orbit of linear operator A in space W . Obviously, an orbit A lies
in some one-dimensional variety, and the system of invariants characterizes this
variety as algebraic.
Definition 4. Polynomial P(b, X ) is called loop invariant if, for any natural j
and any b
(0)
P(b(0) , b( j ) ) 0 .
Theorem 1. If p( X ) r ( X ) q( X ) is an L-invariant of a linear operator A ,
then the polynomial r ( X )q(b) q( X )r (b) is an invariant of a linear loop over the
_
field Q .
We call such loop invariants L-invariants (of linear loops).
Example 2. (a linear loop with operator from example 1)
The linear loop corresponding to the operator A , has the form
(x, y, z) := (a, b, c);
While True|False do (x, y, z) := (y, z, 2*x)
L-invariant of this loop is defined by formula (2):
P( x, y, z, a, b, c) (12 x 1 y z )(32 x 3 y z )(22 a 2 b c) 2
(4)
(22 x 2 y z ) 2 (12 a 1b c)(32 a 3b c)
Note that L-invariant of the loop P( x, y, z, a, b, c) is defined over a field
_
Q(1 , 2 , 3 ) . However, it has a set of L-invariants with coefficients from the field
Q , which can be constructed, they are shown in (4) the canonical form to the
polynomial from 1 , 2 , 3 , and then - to the polynomial from 2 with using the
relation 13 2 and Vieta's relation. Technique for computing L-invariants over a
2
field Q is demonstrated in [20]. Note that if the variables a, b, c are the assigned
numeric values, L-invariant is converted into a loop invariant.
In [22] they described the results, that link L-invariants to eigenvalues and
T
eigenvectors of the operator A . The main result of this work:
Theorem 2 (about the multiplicative relations). Let 1 ,..., m be eigenvalues of a
T
linear operator A and let s1 ,..., sm be eigenvectors of the conjugate operator A
that correspond to these eigenvalues. We assume that there are integers k1 ,..., k m
such that
1k ... m k 1 .
1 m
(5)
Then
p( X ) (s1 , X ) k1 ... (sm , X ) km (6)
is L-invariant of the linear operator A .
Proof of the theorem 2 can be found in [21]
Example 3 (continuation of example 2). Apply the theorem 2 to the example 2.
Calculate the eigennumbers of operator A.
0 1 0 1 0
A 0 0 1 , h ( ) A E 0 1 3 2 .
2 0 0
2 0
A characteristic polynomial has the form b h( x) x 2 . Its roots are
3
1 3 2 , 2 3 2 , 3 3 2 2 , where exp(i 2 3) is the primitive cube
root of unity.
0 0 2
Calculate the eigenvectors s1 , s2 , s3 of matrix A 1 0 0 :
T
0 1 0
s1 (12 , 1 , 1), s2 (22 , 2 , 1), s3 (32 , 3 , 1) .
It is easy to check that 1 2 3 1 . By the theorem 2 the operator A has a L-
2
invariant (2).
Corollary 1. If the minimum characteristic polynomial h(x) of linear operator
A has a free term equal to 1 (i.e. det( A) 1 ), then the linear operator A has
a L-invariant.
Example 4. A loop of the points rotation of a plane (a, b) at an angle
arctan(4 3) .
(x,y) := (a,b);
While True do (x, y):= (4/5*x - 3/5*y, 3/5*x + 4/5*y)
Calculate the eigenvalues and eigenvectors of the operator A :
4 / 5 3 / 5 8
A . h( ) A E 2 1 .
3/ 5 4 / 5 5
4 3 4 3
1 i , 2 i . s1 (i, 1), s2 (i, 1) .
5 5 5 5
Since 12 1 , L-invariant of the operator A is
p( x, y) (ix y)(ix y) x 2 y 2 .
And the loop invariant is x y a b .
2 2 2 2
Example 5. Loop of Fibonacci sequence calculation, starting with a pair of (a, b) .
(x,y) := (a,b);
While True|False do (x, y):= (x + y, x)
Calculate the eigenvalues and eigenvectors of the operator A :
1 1
A . h( ) A E 2 1 .
1 0
1 1 1 1
1 5 , 2 5.
2 2 2 2
1 1 1 1
s1 (1 , 1) ( 5 , 1), s2 (2 , 1) ( 5 , 1) .
2 2 2 2
Since 12 1 , L-invariant of the operator A is
p( x, y) ((1 x y)(2 x y)) 2 ( x 2 xy y 2 ) 2 .
The invariant relation of loop is ( x xy y ) (a ab b ) .
2 2 2 2 2 2
Corollary 2. If the characteristic (minimum) polynomial h(X ) of linear operator
A is x m a , then linear operator has an L-invariants.
Proofs of corollaries 1 and 2 are in [21]
Theorem 3. Let h(x) be an polynomial from variable x with rational
coefficients and (1 ,..., m ) are all its roots in an algebraic closure Q of the
field Q . Consider the set G(h) {x1 1 ... xmm : 11 ... mm 1} that is the set of
k k k k
monomials of the field of rational expressions Q(X ) (possibly with negative
degrees), who receive a value of 1 when we substitute i instead of xi . Then G (h)
is a multiplicative abelian group with a finite number of generators.
The proof of theorem 3 is obvious, since the subgroup of an abelian group with a
finite number of generators has a finite number of generators.
It follows from theorem 3 that the main problem for the generation of L-invariants
is the problem of finding an algorithm for constructing a set that generate the groups
G(h) .
Example 6 (continuation of example 3). It is easy to see that we have the following
multiplicative relations for the polynomial h( x) x 2 between its roots:
3
12 2 3 , 12 32 , 13 22 , 32 33
These relations have relevant binomials
x12 x2 x3 , x1 x2 x32 , x1 x3 x22 , x23 x33 ,
that form a Gröbner basis of the ideal I (GB ) I (G(h)) .
Corollary 3. The set of all L-invariant of operator A defines the field of rational
expressions.
Proof of corollary 3 is in [21]
Theorem 4 Let f (x) be irreducible over the field Q and reduced polynomial and
_
{1, 2 ,...m} is the set of its roots over the field Q . If we have a nontrivial
multiplicative relationship 11 ...mm 1 with integer indices k1 ,..., km between his
k k
m
roots, then the free term am f (x) equal to 1 or k i 0 .
i 1
The proof is in [21]
Definition 5. L-invariants of operator A , defined of multiplicative relation
between the roots of the characteristic polynomial 1 ... m 1, will be called
whole. L-invariants of operator A , defined of multiplicative relation
... 1, ki 0 , will be called rational.
k1
1
km
m
Theorem 5. If the characteristic polynomial of operator A is h( x ), k 1 , then
k
operator A has a rational L-invariants.
The proof of theorem 5 is in [21]
2.2 L-invariants of Jordan Cells
A nondegenerate linear operator A can be represented in a suitable basis by the
following Jordan form of its matrix [18, 22].
J 1 (1 ) 0 ... 0
0 J 2 ( 2 ) ... 0
A , (7)
. . ... .
0 0 ... J m (m )
where J i (i ) are Jordan cells of different sizes. Jordan cell is of the form
1 ... 0
0 ... 0
J ( ) (8)
0 ... 1
0 ... 0
Thus, theorem 2 is applied only to the rows of the matrix of the linear operator A ,
that correspond to the eigenvectors of A , i.e., to the collection of the last rows of
Jordan cells J i (i ) , i 1,..., m . Below, we will extend this theorem to arbitrary
nondegenerate linear operators by considering Jordan cells on the whole.
Transformation J : J * X , where X ( x1 ,..., xk ) , in the coordinate form is
x1 : x1 x2 ;...; xk 1 : xk 1 xk ; xk : xk
df df
Introduce the following notation: xk 1 y, xk z .
For each Jordan cell J k (k ) of the Jordan form of the operator A its own
sequence of subspaces of eigenpolynomials is determined.
The main theory of the eigenpolynomials of Jordan cells as well as of the
relationship between eigenpolynomials and L-invariants of linear operators is
formulated in [23, 24].
The concept of eigenpolynomial of a linear operator can be of an independent
interest for linear algebra applications.
If all eigennumbers of linear operator A are rational numbers, then the problem of
constructing this basis is an algorithmically solvable with the help of
theoretical&number algorithm.
In the [25] a direct method of finding invariants of Jordan cells is described. The
main results of this work are discussed below.
Theorem 6 (about the structure of the ideal of invariants). Let A be an arbitrary
nondegenerate linear operator, presented in a suitable basis of matrix (7),
I J1 ( A),..., I J k ( A) are ideals of his invariants, presented in homogeneous
coordinates
uij xij zi , ui yi / zi eij aij c i , ei bi c i
by basis of the form
u j q j ( , u,1) , j 1,..., n 2
and I (A) is an ideal of invariants of the operator Ared , and I ( A) is an ideal of
invariants of the operator A (of the loop (3)). Then
GBase( I ( A)) GBase( I J1 ( A)) ... GBase( I J k ( A)) GBase( I ( A))
Theorem 7. If a group of multiplicative relations of roots of an irreducible
polynomial f (x) is nontrivial ( MR( f ) (e)) , there may be two situations:
1. The set of roots (1 ,..., n ) is divided into certain number l of equally-
powerful classes 1,..., l ; j {( j 1) d 1,... jd }; j 1,..., l.
wherein d len ( j ), n ld . Multiplicative relations from MR( f ) in this
situation have the form j j , j 1,..., l , where j are roots from 1.
2. The equally-powerful classes 1 ,..., l , i {(i 1) d 1 ,...id }; i 1,..., k.
Wherein d len ( j ), n kd . Multiplicative relations from MR( f ) MR( f )
in this situation have the form i ij j , i 1,..., l , where j are roots from 1.
Both situations may occur simultaneously.
For the proof of theorem 7, take a look in [25]. This theorem has a key role for the
algorithm of calculation of the system generators of the group MR( f ) .
Theorem 8. Let f ( x) Q[ x] is an irreducible polynomial and 1 ,..., m are its
roots. The problem of constructing a basis of a set of generating the group
GU (h) {x1k1 ...xmkm : 1k1 ...kmm U }, where U is a group of all roots from 1 is
algorithmically solvable.
The proof of theorem 8 is in [25].
Thus, by theorem 6, the invariants of a linear operator can be classified as
intracellular - that are inherent to each Jordan cell of linear operator, and intercellular
- those that are inherent in its diagonalisable part.
Intracellular invariants are computed directly from the formulas of [25]
cy bz cy bz
C1 ( ) C n j ( )
z cz cz
x j (a j a j 1 ... a ).
n j
n
c
The existence of intercellular invariants depend on the existence of nontrivial
multiplicative relations between the eigenvalues of the linear operator (theorem 2).
For linear operators with an irreducible minimum characteristic polynomial
problem of constructing a basis of set of multiplicative relations between its
eigenvalues is algorithmically solvable, but the algorithm of theorem 8 is ineffective
due to a very large degree of the polynomial S (x) , which is be necessary to
decompose into factors.
The problem of constructing a basis of set of multiplicative relations for arbitrary
linear operators is still open.
3 The Static Analysis of Linear Inequalities.
Let W K n be an n-dimensional vector space over a linearly ordered and
_
constructive field K and K is an algebraic closure of K .
Definition 6. As a linear semi-algebraic set M ( x1 ,..., xn ) is called the area W ,
that is defined by a quantifier-free formula in the signature of the logical connectives
,&, with linear inequalities in the variables x1 ,..., xn as atoms. If the field
M is given by the formula F (X ) , i.е. М {X : F(X)} , We shall denote it by
M ( F ( X )) .
Definition 7. Let X ( x1 ,..., xn ), and b (b1 ,..., bn ) be two vectors of
variables. The linearly loop with the precondition is a fragment of imperative program
in the form
X := b; // S (b ) - a precondition
While U(X, b) do X := A*X (9)
where S (b ) , and U ( X , b ) are quantifier-free formulas of applied logic of linear
semi-algebraic sets, A is a matrix of the linear operator W W .
Non-deterministic and associated with loop (9) we call the loop of the form
X := b; // S (b ) - a precondition
While True|False do X := A*X (10)
whose number of repeats is nondeterministic.
Remark 2. Definition 7 of loops differs from the definitions 2 and 3 because of its
precondition S (b ) that limited the initial values of the loops variables by a linear
semi-algebraic set and an introduction to the consideration of the conditions of the
loop U ( X , b ) .
Definition 8. Linear inequality P( X , b) K [ X , b] is called an invariant for the
1
loop (9) with a precondition S (b) , if it is executed whenever the loop body is
executed.
df
P( X , b) a1 x1 ... an xn a1' b1 ... an' bn
Thus, the invariance means performing of a sequence of formulas
S (b) P(b, b) , // Invariant is executed in the input in the loop
U (b, b) P( Ab, b) , // Invariant is executed after the first iteration
U ( Ab, b) P( A2 b, b) , // Invariant is executed after the second iteration
…
U ( Ak b, b) P( Ak 1b, b) , // Invariant is executed after the k-th iteration
U ( Ak b, b) P( Ak b, b) // Invariant is executed at the completion of the
loop
Theorem 9. If all eigenvalues (1 ,..., n ), i K of operator A are real,
the problem of proving of the invariance P( X , b) for the loop (9) is algorithmically
solvable.
The main content of the proof of theorem 9 is formulated in lemmas 1-5 [13].
Definition 9. The linearly defined loop (10) is called completed if for any
b M (S ( X )) the sequence
b (0) b , b ( m 1) Ab ( m) , m 0,1,... (11)
for some natural m* m * (b ) satisfies the relationship U (b
( m*)
,b ) .
Thus, if the loop is completed, for each b M ( S ( X )) is the smallest positive
integer m * (b ) , on which the loop (9) is completed.
Definition 10. Let a , c K . A linear inequality
n
df
L(a , c , X , b ) (a , X ) (c , b ) (12)
is called conditional invariant of linear certain loop (9) (with a precondition
S (b ) ), if for any b M ( S ( X )) Orbit( A, b ) (11) is satisfies to relations
S (b ) L(a , c , b , b ) , U (b ( m1) , b ) L(a , c , b ( m) , b ), m 1,2,..., m * (b ) .
Remark 3. If the loop (10) is not completed (is branched) at some point b ,
m * (b ) it should be considered equal to infinity.: m * (b ) .
Example 7.
S ( x, y) (0 x 1) & (0 y 1) ,
U ( x, y, b1 , b2 ) (| x b1 | ) & (| y b2 | ) ,
3 / 5 4 / 5
A .
4 / 5 3 / 5
L x y 2b1 2b2 // a (1,1), c (2, 2) .
b
L(a, c , X , b )
U ( X , b )
Fig. 2. Geometric illustration of the linear defined loop.
In this example, the linear operator A is an operator of rotation for
angle arctg (4 / 3) . A starting point b belongs to the unit square. The orbit of a
linear operator A is a sequence, each point of which lies on the loop
x y b b22 . The condition of repeating of the loop is a «point ( x, y) that
2 2
1
2
lies outside the square with side 2 and center at (b1 ,b2 ) ». Therefore, a loop is
completed when the point gets inside this square, i.e. a point will make the rotation by
angle 2k with accuracy equal to . Since the angle is incommensurate
with , the orbit of the operator A is a dense set on the circle x y b1 b2 ,
2 2 2 2
therefore, the loop is complete. In this example, the basic algorithm is used to prove
that L x y 2b1 2b2 is a conditional invariant of loop.
Let f (x) be a minimal characteristic polynomial of the operator A ,
{1,..., n } is a set of its roots (spectrum A ). Suppose further that, 1 ,..., 2 k
is a set of complex eigenvalues, and 2 k 1 ,..., n is a set of real eigennumbers
and 1 2 ,..., 2 k 1 2 k than we obtain a representation of a linear operator in
the so-called real Jordan form:
B1 0 . 0 . . 0
0 B2 . 0 . . 0
. . . . . . .
A 0 ... 0 Bk . ... 0
0 . . 0 2 k 1 ... 0
. . . . . . .
0 ... n
. . . 0
j j
B j rj
j .
Where
j
Remark 4. After the transition to a basis of eigenvectors the coefficients of
inequality will be changed. If S () is a transition matrix, then the new values of the
1 1
vectors a, b calculated by the formulas a Sa S , b Sb S . But in order
(S ) (S )
not to overload the text by new notations, we will use the old notations.
df
Note, that the matrix of the form B , where 1 is a matrix
2 2
of rotation of vector of two-dimensional space on the angle , that is defined by
ratios cos( ) , sin( ) . That is why
cos( j ) sin( j )
B j rj
sin( j ) cos( j ) , r j j j 2 j 2 .
inequality (12), whose invariance is regarded by a loop (11) with a specific initial
value b , indicates that X Orbit( A, b )(a , X ) (c , b ) . Algorithm of prove of
the invariance of (12) will be formulated in the equivalent form:
Sup ( a , X ) (c , b ) .
X Orbit( A, b )
df
Let us consider the linear form a1 x1 a2 x2 ... an xn (a , X ) . The
transformation X : A * X converting this form in (a, AX ) , and m is a multiple
m
iteration of loop, that is described by the transformation X : A * X - in
(a, Am X ) .
X1 ( x1, x2 ),..., X k ( x2k 1, x2k ) a1 (a1, a2 ),..., ak (a2k 1, a2k )
Let , .
Then
(a , X ) (a1, X1 ) ... (ak , X k ) a2k 1x2k 1 ... an xn
(13)
Conversion (a , AX ) of a linear form can be written as
(a , AX ) (a1 , B1 X 1 ) ... (ak , Bk X k ) 2k 1a2k 1 x2k 1 ... n an xn
(14)
And its m -th iteration can be written as
(a , Am X ) (a1 , B1m X 1 ) ... (ak , B km X k ) m2 k 1 a2k 1 x2k 1 ... mn an xn (15)
Passing in (14) to the representation in the form B j r j B j , we obtain:
(a , Am X ) r1m (a1 , B1m X 1 ) ... rkm (ak , B km X k ) m2 k 1 a2 k 1 x2k 1 ... mn an xn
Consider the question of the set of values of the operator orbit
(a1 , B1 X 1 ) ... (ak , B k X k ) for the initial value b
m m ( 0)
(b ,..., b ) , where
1
( 0)
k
( 0)
b j (b2 j 1, b2 j ) , j 1,..., k . The interpreted pair X j shall be as points on the two-
df cos( j ) sin( j )
dimensional plane, and the conversion of B j - as a
sin( j ) cos( j )
rotations of points X j on the angle j .
The proof is formulated in lemmas 1-7 in [20].
Theorem 10. The problem of proving the invariance of inequality L(a , c , X , b )
for the loop (9) with diagonalizable linear operator A and with an initial point b is
algorithmically solvable.
Theorem 11. The problem of proving the invariance of inequality L(a , c , X , b )
for the loop (9) (i.e., with the precondition S (b) ) is algorithmically solvable.
Theorem 12. The problem of termination of the loop (9) is algorithmically
solvable. Proof of theorems 10-12 is in [20].
4 Conclusion
This review represents main results of several works of one of the authors of the
theory of program invariants. Subject of the research is an invariant of linear iteration
loops. A new approach to the problems of static analysis of linear loops is
represented: the problem of generating of polynomial invariance equations and the
problem of proving the invariance of linear inequalities. This approach uses the
representation of a linear operator in the loop body in the Jordan form and is based on
the analysis of the spectrum of this operator.
The main results about invariant equality are the theorem 2 about multiplicative
relations, a formula of invariant equations for the Jordan cell, a theorem 6 of the
structure of a basis of the ideal of polynomial invariants, and, also, the algorithm of
constructing of the basis of ideal of polynomial invariants for operators with
irreducible over the field of rational numbers characteristic polynomial. Thus, for a
given problem the problem of constructing of the basis of ideal of polynomial
invariants for operators with a reducible characteristic polynomial remains open.
From the practical view, the interest is in constructing the corresponding effective
algorithms.
Unlike polynomial equations, the set of linear invariant inequalities does not have a
finite basis. Therefore, a method of generating the basis is not applicable to this task.
This paper represents the basic idea of the direct method of proof of the invariance of
linear inequalities. There is a need to note, that the key role in the method is played by
the set of maximal (from the modulus) eigenvalues of operator A . In this case, the
case of maximal real eigenvalues and the maximal complex eigenvalues are
significantly different. In the second case, the method uses the original method of
finding the maximum of the linear form in the orbit of a linear operator, and various
algorithms of computation in the field of algebraic number.
There is a need to assume that this method can be used as a basis for a general
algorithm of proving the invariance of a system of linear inequalities for linear-certain
programs, similar to the method of proof of invariance of polynomial equations [5, 6],
and to prove the invariance of polynomial inequalities for linear-certain programs.
References
1. Floyd, R.: Assigning Meanings to Programs. In: Proceedings of Symposium on Applied
Mathematics, J.T. Schwartz (Ed.), American Mathematical Society, vol. 19, pp. 19--32,
Providence, R.I. (1967)
2. Hoare, C.: An Axiomatic Basis for Computer Programming. Communications of the ACM
12(10), 576--580 (1969)
3. Letichevsky, A..: About One Approach to Program Analysis. Cybernetics 6, 1--8 (1979)
4. Godlevsky, A., Kapitonova, Y., Krivoy, S., Letichevsky, A.: Iterative Methods of Program
Analysis. Cybernetics 2, 9--19 (1989)
5. Letichevsky, A., Lvov, M.: Discovery of Invariant Equalities in Programs over Data Fields.
Applicable Algebra in Engineering, Communication and Computing 4, 21--29 (1993)
6. Müller-Olm, M., Seidl, H.: Precise Interprocedural Analysis Through Linear Algebra. In:
Proc. of Symposium on Principles of Programming Languages, pp. 330--341, ACM, New
York (2004)
7. Lvov M.: About One Algorithm of Program Polynomial Invariants Generation. Technical
report, RISC Report Series (2007) (electronic).
8. Müller-Olm, M., Seidl, H.: Computing Polynomial Program Invariants. Inf. Process. Lett.
91(5), 233--244 (2004)
9. Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear Loop Invariant Generation Using
Gröbner Bases. In: Proc. of Symposium on Principles of Programming Languages, pp. 318--
329, ACM, New York (2004)
10. Caplain, M.: Finding Invariant Assertions for Proving Programs. In: Proc. of the intern.
Conf. on Reliable Software, pp. 165--171, ACM, New York (1975)
11. Rodríguez-Carbonell, E., Kapur, D.: Automatic Generation of Polynomial Loop Invariants:
Algebraic Foundations. In: Proc. Of International Symposium on Symbolic and Algebraic
Computation, pp. 266--273, ACM, New York (2004)
12. Rodríguez-Carbonell, E., Kapur, D.: Automatic Generation of Polynomial Invariants of
Bounded Degree Using Abstract Interpretation. Sci. Comput. Program 64(1), 54--75 (2007)
13. Lvov, M.: A Method of Proving the Invariance of Linear Inequalities for Linear Loops.
Cybernetics and Systems Analysis 4, 80--85 (2014)
14. Kovács, L. I., Jebelean, T.: An Algorithm for Automated Generation of Invariants for
Loops with Conditionals. In: Proc. of Intern. Symposium on Symbolic and Numeric
Algorithms for Scientific Computing. pp. 245--249, IEEE Computer Society, Timisoara
(2005)
15. Kurosh, A.: Theory of Groups. 3-rd ed. Science, Moscow (1967)
16. Postnikov, M.: Galois Theory. Fizmatgiz, Moscow (1963)
17. Buchberger, B:. Gröbner Bases. An Algorithmic Method in the Theory of Polynomial
Ideals. Computer algebra. Symbolic and algebraic computations. Mir, Moscow (1986)
18. Van Der Waerden: Algebra, B. the 2-th edition. GRFML, Moscow (1979)
19. Dieudonné, J. Carroll, Dj. Mumford, D.: Geometric Invariant Theory. Mir, Moscow (1974)
20. Lvov, M.: Analysis of Linear Defined Iterative Loops. Cybernetics and Systems Analysis 4
(2015) (In print)
21. Lvov, M.: Polynomial Invariants for Linear Loops. Cybernetics and Systems Analysis 4,
159--168 (2010)
22. Hodge, V., Pido, D.: Methods of Algebraic Geometry, Moscow (1954)
23. Lvov, M., Kreknin, V.: Nonlinear Invariants for Linear Loops and Eigenpolynomials of
Linear Operators. Cybernetics and Systems Analysis 2, 126--139 (2012)
24. Kreknin, V., Lvov, M.: Eigenpolynomials of Linear Operators and Polynomial Invariants of
Linear Loops of Program. Scientific Journal NEA Dragomanov 1(11), 150—169 (2010)
25. Lvov, M.: On the Structure of Polynomial Invariants of Linear Loops. (In print)
26. Cousot P., Halbwachs N.: Automatic Discovery of Linear Restraints among Variables of a
Program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, pp. 84--97, ACM Press, New York (1978)
27. Krivoy, S., Raksha, S.: Search of Invariant Linear Dependencies in Programs. Cybernetics
6, 23--28 (1984)
28. Godlewski, A., Kapitonova, Y, Krivoy, S., Letichevsky, A.: Iterative Methods of Programs
Analysis. Equalities and Inequalities. Cybernetics 3, 1--10 (1990)
29. Lvov, M.: Invariant Inequalities in Programs Interpreted over an Ordered Field. Cybernetics
5, 22--27 (1986)
30. Lvov, M.: About Invariant Inequalities for States of the Program Schemes, that Interpreted
Over the Vector Space. Cybernetics 2, 111--112 (1985)
31. Lvov, M.: A Method of Proving the Invariance of Linear Inequalities for Linear Loops.
Cybernetics and Systems Analysis 4, 80--85 (2014)