Tree Constraint Solver (TCS) - Linear tree inequality solver for superlinear resource bounds on Java programs

这个项目的目的是提供可证明的正确上限的资源消耗的无注释的面向对象的Java程序。这种自动资源分析已经变得越来越受欢迎，具有相当大的工业兴趣，但迄今为止主要局限于函数程序和经典的命令式程序与数组作为唯一的基本数据结构。我们建立在基于类型的摊销分析，这已被应用于函数式编程语言取得了巨大成功的良好的框架。面向对象编程提出了几个新的挑战：a）数据结构通过类隐式定义，但不像函数数据类型声明那样显式给出，B）命令式更新可能导致复杂的别名，c）更通用的数据结构，如双向链表，甚至通用图都是可能的。在早期的工作中，这些挑战是解决减少资源约束的问题，一个创新的约束系统，涉及无限多的数值变量（“线性树约束（LTC）”）。然而，那里提出的启发式约束求解器仅限于某些特殊情况。在最近的工作中，它表明，一般的LTC是可判定的，因此在实践中也可能是易处理的，本项目的目的是详细探讨这一点。具体地说，我们将开发和实现一个有效的解决方案算法一般LTC，也提供了具体的上限堆空间消耗的程序。为此，仅可判定性是不够的，我们还需要在封闭公式中检测约束的最小解。此外，我们将确定和证明决策问题的精确复杂性，并找到一个新的，更好的算法，福尔斯属于这个复杂性类。现在得到的可判定性结果是一个很好的起点，使计划可能workedout.We将使用这些结果来设计一个基于类型的摊销资源分析的命令式面向对象的程序，并测试它的各种示例程序的原型实现的基础上Java语法。

This project aims to provide provably correct upper bounds on the resource consumption of unannotated object-oriented Java programs. Such automatic resource analysis has become increasingly popular with considerable industrial interest but was hitherto mostly confined to functional programs and classical imperative programs with arrays as the only essential data structure. We build upon the well-established framework of type-based amortized analysis, which has been applied to functional programming languages with great success. Object-oriented programming poses several new challenges: a) data structures are implicitly defined through classes, but not explicitly given as in functional datatype declarations, b) imperative updates may lead to complex aliasing, c) more general data structures like doubly-linked lists, or even general graphs are possible. In earlier work, these challenges were addressed with a reduction from the resource bound question to an innovative constraint system involving infinitely many numerical variables (”linear tree constraints (LTC)”). However, the heuristic constraint solver that was presented there was limited to certain special cases. In very recent work, it was shown that the general LTC are decidable and thus might be also tractable in practice and the aim of this project is to explore this in detail. Concretely, we will develop and implement an efficient solution algorithm for general LTC that delivers also concrete upper bounds on the heap space consumption of programs. For that, decidability alone is not sufficient, we also need to detect minimal solutions to the constraints in terms of closed formulas. Further, we will determine and prove the exact complexity of the decision problem and find a new, better algorithm that falls into this complexity class. The decidability result obtained by now is a good starting point that makes the plan likely to work out.We will then use these results to design a type-based amortized resource analysis for imperative object-oriented programs and test it on a variety of example programs with a prototype implementation based on Java syntax.