Synthetic programming

摘要

Given a formal specification for a desired program, our goal is to transform it step-by-step into executable code. We proceed in a top-down fashion—as suggested by ‘structured programming’ methodology. Each step consists of applying a synthesis rule to rewrite a segment of the developing program in increased detail. If every step is transparent enough to ensure correctness, each partial program in the series is sure to be equivalent to its predecessor. In particular, the final program is guaranteed to satisfy the initial specifications.