Encoding and decoding in refinement algebra

Refinement algebras are axiomatic algebras for reasoning about programs in a total-correctness framework. We extend demonic and angelic refinement algebra with operators for encoding and decoding. Encoding gives one the least data refinement of a program with respect to a given data-refinement abstraction. Decoding gives one the greatest program that can be data refined into the decoded program with respect to a given abstraction statement. The resulting algebra is applied to reasoning about action systems