A Method of Proving the Invariance of Linear Inequalities for Linear Loops
- PDF / 103,979 Bytes
- 6 Pages / 594 x 792 pts Page_size
- 52 Downloads / 143 Views
SOFTWARE–HARDWARE SYSTEMS A METHOD OF PROVING THE INVARIANCE OF LINEAR INEQUALITIES FOR LINEAR LOOPS UDC 004.421.6
M. S. Lvov
Abstract. This article presents a new method for proving the invariance of simultaneous linear inequalities for iteration loops defined over the field of rational numbers with a linear operator in the loop body. The method takes into account a loop precondition in the form of a system of linear inequalities. The consideration is restricted to the case when all eigenvalues of the linear operator are real. The method is based on computing the number of loop iterations whose execution either ensures or disproves the invariance of the system of linear inequalities. The method uses the Jordan form of representation of linear operators. Keywords: static program analysis, linear invariant of a loop, invariant system of linear inequalities. INTRODUCTION The problem of searching for invariants at control points of imperative programs is posed by R. Floyd [1] and S. Hoare [2] as the key problem of analysis of properties of programs. In investigating this problem, the emphasis was on the problem of constructing polynomial invariants such as equalities. A set of invariants of the type of equality forms a polynomial ideal whose finite basis should be constructed. In the general case, the problem of construction of such a basis has not been solved yet. In [3], general iterative methods of generation of program invariants are proposed that can be applied in many object domains. In [4–7], a method is presented for proving the invariance of a polynomial and constructing the basis of the vector space of polynomial invariants of bounded degree. In [8], the solution of problems of constructing the basis of the vector space of polynomial invariants is given for the class of programs with procedures performing only linear computations. Many works, for example, [9–13] are devoted to a more partial but the key problem of construction of invariant equalities for iterative loops. In particular, the problem of constructing the basis of the ideal of polynomial invariant equalities for linear loops is investigated in [11–13]. The problem of the description of invariant inequalities is less studied. Here, the main intricacy lies in the infinity of the basis of the metaideal of polynomial inequalities [12, 13]. Iterative methods for solving the problem of the description of linear invariant inequalities were considered in [14–17]. In [14], the problem of generation of simplest invariant inequalities is solved. In [15, 16], general iterative methods are used to solve the problem of searching for linear invariant inequalities. The mathematical definitions and results that are used in this article can be found, for example, in [19, 20]. MAIN RESULTS Definition 1. Let Q n be an n- dimensional vector space over the field of rational numbers Q, and let Q be the algebraic closure of the field Q. Definition 2. Let X = ( x1 , ... , x n ) and b = ( b1 , ... , bn ) be two vectors of variables. A linear loop with a precondition is
Data Loading...
