Encoding, Decoding and Data Refinement
Ralph‐Johan Back, Joakim Wright · Formal Aspects of Computing · 2000
Abstract. Data refinement is the systematic replacement of a data structure with another one in program development. Data refinement between program statements can on an abstract level be described as a commutativity property where the abstraction relationship between the data structures involved is represented by an abstract statement (adecoding). We generalise the traditional notion of data refinement by defining anencoding operatorthat describes the least (most abstract) data refinement with respect to a given abstraction. We investigate the categorical and algebraic properties of encoding and describe a number of special cases, which include traditional notions of data refinement. The dual operator of encoding isdecoding, which we investigate and give an intuitive interpretation to. Finally we show a number of applications of encoding and decoding.