Program refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program.