Calculating Encoding And Decoding Functions For Prefix Codes
ACM SIGPLAN Notices(1999)
摘要
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 nontrivial 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 functional program, dealing successively with correctness and time efficiency, as well as the key decisions that are adopted.
更多查看译文
关键词
functional programming,program specification,assertions,program synthesis,function inversion,program transformation,verification,ADTs
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络