Transformational Derivation in the Programming Logic TK
Martin C. Henson · 1992
We examine transformational programming techniques within the programming logic TK. In particular we investigate the transformational technique known as type simulation. The internalisation of this technique within TK is illustrated with respect to a derivation of the a-b-pruning algorithm from a specification of mini-maxing. 2 Introduction In this paper we investigate transformational programming techniques within the programming logic TK. This theory has been elaborated in detail in [HeT88] and some aspects of program development within TK are explored in [Hen89a]. Our point of departure here is the transformational technique known as type simulation [Hen88] which is a generalisation of a idea due to Wand [Wan80]. We must, for reasons of space, refer the reader to the references for an detailed exposition of the programming logic TK. For the same reason most of the technical results of Section 4 are stated here without detailed proof. The interested reader may like to consult [Hen8...