Towards an automated tool for computing loop functions

Despite several decades of on-and-off research efforts, the functional analysis of computer programs to an arbitrary level of thoroughness and precision remains an unfulfilled challenge. Also, despite several decades of advances in programming language design and implementation, most of the software that is written and maintained today is written in traditional imperative programs; in such programs, the most critical/most complex control structure is the loop. In this paper, we discuss our ongoing effort to develop a tool that reviews a while loop written in an imperative language (C, C++, Java) and derives its function, by specifying the final values of all its program variables as a function of its initial values.