Retrograde Program Analysis: A Practical Tutorial

TL;DR

This paper provides a practical tutorial on retrograde program analysis, explaining how to analyze programs backward from outputs to inputs using examples, formal methods, and standardized techniques.

Contribution

It offers a concise, accessible guide with definitions, examples, and standardized methods for retrograde analysis, facilitating practical application and understanding.

Findings

Effective for analyzing program correctness from outputs to inputs

Includes worked examples like sorting networks and binary search

Provides standardized techniques for array splits and midpoints

Abstract

Retrograde analysis reads programs from the end to the beginning: treat statements as constraints on prior states, propagate sets of states backward, and compare the reachable inputs with the intended specification. This tutorial condenses a longer exposition to a focused guide with definitions, worked examples (toy branches, sorting networks, binary search), loop treatment via fixpoints, and a range-algebra appendix that standardizes array splits and midpoints. The aim is practical: short proofs, concrete invariants, and drop-in code and property tests