Toward the Automated Derivation of Loop Functions

Modern software applications are growing increasingly large and complex, at the same time as they are taking on increasingly critical roles. To deal with this twofold pressure, we need automated tools that help us analyze the function of programs or program fragments to an arbitrary level of precision. This paper discusses an approach to computing the function of a while loop, and illustrates it by means of a simple prototype.