Scaling step-wise refinement

TLDR

Step‑wise refinement is a powerful paradigm for developing a complex program from a simple program by adding features incrementally. The authors present the AHEAD model to demonstrate how step‑wise refinement can scale to synthesize multiple programs and noncode representations. The approach uses the AHEAD model together with a supporting tool set to enable synthesis of multiple programs and noncode representations. AHEAD shows that software can be expressed as nested sets of equations and that its tools can automatically refine Java and nonJava artifacts from equational specifications, a capability previously achieved only by ad hoc methods.

Abstract

Step-wise refinement is a powerful paradigm for developing a complex program from a simple program by adding features incrementally. We present the AHEAD (algebraic hierarchical equations for application design) model that shows how step-wise refinement scales to synthesize multiple programs and multiple noncode representations. AHEAD shows that software can have an elegant, hierarchical mathematical structure that is expressible as nested sets of equations. We review a tool set that supports AHEAD. As a demonstration of its viability, we have bootstrapped AHEAD tools from equational specifications, refining Java and nonJava artifacts automatically; a task that was accomplished only by ad hoc means previously.