Next-generation software engineering is envisioned as a computational discipline that complements human capability through automated computation of software behavior and properties to the maximum extent possible. To help realize this vision, we are exploring the technology of function extraction. Behavior computation for sequences and alternations is relatively straightforward, but no general theory for loop computation can exist, and engineering solutions must be sought. This paper defines an infrastructure for loop computation based on hierarchies of semantic recognizers operating within a refinement calculus, and outlines an extraction algorithm for computing loop behavior based on application of the recognizers.
Ali Mili, Tim Daly, Mark Pleszkoch, Stacy J. Prowe