Program synthesis is the derivation of a program from a specification. When the synthesis is done according to semantically correct TransformationRules the resulting program is a correct implementation of the specification. *See Also* * BirdMeertensFormalism: calculus for deriving programs * ProgramCalculation: methodology for deriving implementations from specifications (synonym) * SpecWare: a system for semi-automatic program synthesis * ADATE: Automatic Design of Algorithms Through Evolution (ADATE) is a system for automatic programming i.e., inductive inference of algorithms