Diego Alonso, On the Limits of the Classical Approach of the Cost Analysis
On the Limits of the Classical Approach of the Cost Analysis
Several cost analysers follow the classical approach to cost analysis. In this approach, the cost of each program's module is specified as a function of the program's inputs sizes, and these functions are inferred by
- transforming each program module into a system of recurrence relations, that model the program's cost: and
- solving these recurrence relations, which can be done with common computer algebra systems.
In this paper we show the limits of this approach, namely, that analysers following it obtain asymptotically imprecise results for certain programs. We then present another approach for the verification and synthesis of cost bound functions based on first-order Satisfiability and Quantifier Elimination that can infer precise results for those programs.