Calculating Polynomial Runtime Properties

Affine size-change analysis has been used for termination analysis of eager functional programming languages. The same style of analysis is also capable of compactly recording and calculating other properties of programs, including their runtime, maximum stack depth, and (relative) path time costs. In this paper we show how precise polynomial bounds on such costs may be calculated on programs, by a characterization as a problem in quantifier elimination. The technique is decidable, and complete for a class of size-change terminating programs with limited-degree polynomial costs. An extension to the technique allows the calculation of some classes of exponential-cost programs. We demonstrate the new technique by recording the calculation in numbersof-function (or procedure) calls for a simple definition language, but it can also be applied to functional and imperative languages. The technique is automated within the reduce computer algebra system.

• Type: Conference
• Year: 2005
• Where: APLAS
• Authors: Hugh Anderson, Siau-Cheng Khoo, Stefan Andrei, Beatrice Luca
• Keywords: APLAS 2005, Eager Functional Programming, Path Time Costs, Precise Polynomial Bounds