Polynomial recursion analysis in pascal like programs

Abstract

Besides being of theoretical interest the knowledge about a procedure's calling behavior is valuable for an optimizing compiler. It is well known, however, that such properties like recursivity or reachability of procedures are unfortunately undecidable for programs in ALGOL-like languages and are still worse than P-Space Complete in the ISO-Pascal case.

We extend this language hierarchy (with respect to parameter restrictions) at the lower end to Wirth's Pascal and show that there the recursivity problem for procedures is decidable within polynomial time. In order to establish this (rather unexpected) result we

• 1. reduce recursivity of a procedure to a reachability problem — with both properties being defined on an infinite tree representation of the program;

• 2. show the equivalence between reachability in such an infinite tree on the one hand and reachability in the finite graph representation on the other hand;

• 3. solve then the reachability problem in this graph in O(ns) of a program with n procedures as vertices and s call statements as edges.