An Analysis of Program by Symbolic Computation

Abstract

<p> We present a symbolic analysis of a class of while loop programs which can automatically derive a closed-form symbolic expression for the input-output relation embodied in that program.</p> <p> We show that this is especially well-suited to analyzing programs from scientific computation, in particular programs which compute special functions (like Bessel functions) from its Taylor series expansion. Other than making heavy use of algebraic manipulations, as available in any computer algebra system, we also require the use of recurrence relations. It is from these recurrence relations that we derive most of our information.</p> <p> It is important to note that we can often get interesting information about a program (like termination) without requiring closed-form solutions to the recurrences.</p>