On ranking functions for single-path linear-constraint loops
- PDF / 378,689 Bytes
- 12 Pages / 595.276 x 790.866 pts Page_size
- 6 Downloads / 211 Views
STTT Regular Paper
On ranking functions for single-path linear-constraint loops Yi Li1 · Wenyuan Wu1 · Yong Feng1
© Springer-Verlag GmbH Germany, part of Springer Nature 2019
Abstract Program termination is a fundamental research topic in program analysis. In this paper, we present a new complete polynomialtime method for the existence problem of linear ranking functions for single-path loops described by a conjunction of linear constraints, when variables range over the reals (or rationals). Unlike existing methods, our method does not depend on Farkas’ Lemma and provides us with counterexamples to existence of linear ranking functions, when no linear ranking function exists. In addition, we extend our results established over the rationals to the setting of the integers. This deduces an alternative approach to deciding whether or not a given SLC loop has a linear ranking function over the integers. Finally, we prove that the termination of bounded single-path linear-constraint loops is decidable over the reals (or rationals). Keywords Software reliability · Program termination · Linear ranking functions · Farkas’ lemma
1 Introduction Proving termination of loops in programs is an important problem whose solutions can broadly improve software reliability. A standard technique to prove the termination of a loop is to find a ranking function, which maps program states to elements of some well-founded ordered set, such that the value descends whenever the loop completes an iteration. Several methods for synthesizing ranking functions have been suggested [2,4,5,8,10–13,17,20,22,26]. And the complexity of the linear ranking function problem for linearconstraint loops is discussed in [3,5]. In this paper, we focus on single-path linear-constraint loops (SLC loops for short), which are specified by a conjunction of linear constraints. For SLC loops, inequalities in their loop bodies may arise due to abstraction. We now take an example from [5] to describe such loops. The loop with two integer variables x1 , x2 ,
B
Yi Li [email protected] Wenyuan Wu [email protected] Yong Feng [email protected]
1
Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences, Chongqing, China
while (4x1 ≥ x2 ∧ x2 ≥ 1) do {x1 := (2x1 + 1)/5; x2 := x2 }, whose loop body consists of deterministic update statements, can be represented by linear constraints: while (4x1 ≥ x2 ∧ x2 ≥ 1) do {5x1 ≤ 2x1 + 1; 5x1 ≥ 2x1 − 3; x2 = x2 }.
(1)
The latter is usually called an SLC loop, where the loop body is interpreted as expressing a relation between the new values (x1 , x2 ) and the previous values (x1 , x2 ). Generally, this representation allows nondeterminism. Obviously, the above SLC loop is specified by a system of linear inequalities: {4x1 ≥ x2 , x2 ≥ 1, 5x1 ≤ 2x1 +1, 5x1 ≥ 2x1 − 3, x2 = x2 }. More examples of programs with nondeterministic update statements can be found in [2,5,8,13]. As a special class of ranking functions, linear ranking functions (LRFs) are widely used in termination analysis of S
Data Loading...
