R.everse Execul.ion of Programs

The transformational model of program development allows obtaining programs correct by construction. When developing nontrivial programs, three activities arise: program synthesis, program transformation, and verification of properties; in addition, specification, use and implementation of ADTs must typically be considered all through these activities. The purpose of this article is to illustrate the need for all these activities by means of a nintrivial problem: encoding and decoding with prefix codes. Our exposition is rather informal, not being committed to any particular program transformation system, and it should be understood by any programmer looking forward to develop functional programs in a systematic way, while avoiding the burden of any particular system. in. particular, we show the stages in the complete transformational development of a functiona.l prograin, dealing successively with correctnessand time efficiency, as well as the key decisions that are adopted. Keywords: Functional programming, program specification, assertions, program synthesis, function inversion.Aprogram transformation, verification, ADTs.