In computer science, program derivation is the derivation of a program from its specification, by mathematical means.