We consider the following problem: given a program, find tight asymptotic bounds on the values of some variables at the end of the computation (or at any given program point) in terms of its input values. We focus on the case of polynomially-bounded variables, and on a weak programming language for which we have recently shown that tight bounds for polynomially-bounded variables are computable. These bounds are sets of multivariate polynomials. While their computability has been settled, the complexity of this program-analysis problem remained open. In this paper, we show the problem to be PSPACE-complete. The main contribution is a new, space-efficient analysis algorithm. This algorithm is obtained in a few steps. First, we develop an algorithm for univariate bounds, a sub-problem which is already PSPACE-hard. Then, a decision procedure for multivariate bounds is achieved by reducing this problem to the univariate case; this reduction is orthogonal to the solution of the univariate problem and uses observations on the geometry of a set of vectors that represent multivariate bounds. Finally, we transform the univariate-bound algorithm to produce multivariate bounds.
翻译:我们考虑以下问题: 给一个程序, 在计算( 或任何给定程序点) 的输入值的结尾处, 找到某些变量值的严格零点界限 。 我们集中关注多球基变量的案例, 以及我们最近显示多球基变量的严格界限是可比较的薄弱编程语言 。 这些界限是多变量多变量组合的组合。 虽然它们的可比较性已经解决, 程序分析问题的复杂性仍然未解决 。 在本文中, 我们显示问题为 PSPACE 已完成 。 主要贡献是一个新的、 空间效率分析算法 。 这个算法是在几步中获得的。 首先, 我们为单球基变量组合开发一种算法, 一个小问题已经很难解决 。 然后, 通过将这个问题降低到 单数组合, 程序的复杂性仍然未解析 。