• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Encoding, Decoding and Data Refinement

Ralph-Johan Back, Joakim von Wright, Encoding, Decoding and Data Refinement. Formal Aspects of Computing 12, 313–349, 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 (a decoding). We generalise the
traditional notion of data refinement by defining an encoding operator that 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 is decoding, which
we investigate and give an intuitive interpretation to. Finally we show a number of applications of
encoding and decoding.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jBavo00a,
  title = {Encoding, Decoding and Data Refinement},
  author = {Back, Ralph-Johan and Wright, Joakim von},
  journal = {Formal Aspects of Computing},
  volume = {12},
  pages = {313–349},
  year = {2000},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Publication Forum rating of this publication: level 2

Edit publication