College of Computing Sciences

Functional Extraction Project

The aim of this project is to extract the function of while loops, written in traditional programming languages (such as C++, Java, etc) in an automatic fashion.  While this is related to work on loop invariant generation, it differs from it in two important details:  first it aims to derive the function of the loop rather than a loop invariant for it; second, we use Mills' logic of programming (rather than Hoare's logic).  The first difference has a crucial implication:  whereas loop invariants depend on the loop and its precondition and post-condition, loop functions depend solely on the loop, and not on the context in which it is used.

The loop extraction proceeds in three steps:  in the first step we map the loop from its programming language notation (in C++, Java, C, etc) to a uniform internal representation;  in the second step we analyze this uniform representation to generate equations between initial states and final states; in the third step we submit the equations to Mathematica so that it resolves the equations in the final states as a function of the initial states. 

The theory behind our approach is presented in this (yet unpublished) paper.  An Outline of the algorithm for the second step (which we have since written in C++) is presented in this paper (published in HICSS 2007).  And (very) preliminary results of the automated extraction are presented in this paper (published in SEW 2007).  This paper (published in WING 2007) discusses the differences between ttraditional loop invariant generation and our work.