e/Refinement calculus

Information
has gloss	eng: Refinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an efficiently executable program.
lexicalization	eng: Refinement Calculus
instance of	c/Formal specification languages