Martin Schwenke

The Essence of Expression Refinement

Martin Schwenke and Brendan Mahony

Abstract

Expression refinement semantics are often complex. In particular, semantics for the relatively simple notion of function application are often disproportionately complex. Monads are frequently championed as the `right' tool for structuring the semantics of function application. In this paper, we consider the interaction between monadic semantics and refinement semantics. We demonstrate that a monad extended with a refinement ordering becomes an elegant tool for structuring the semantics of expression refinement. We do not claim that using monads to structure the semantics of function application is a new idea, nor do we introduce novel semantic models for non-deterministic languages. We simply demonstrate that the structure provided by monads ensures a consistent semantic approach. We illustrate this further by adding a facility for output to one of our languages.

Download

• essence.pdf
  Last modified: 2007-12-20 17:31:08.
  147KB.

This version of the paper contains the following fixes compared to the originally published version:

• The semantic brackets have been dropped from the right-hand sides of equations (13), (20), (26), (32), (41) and (47). This means that refinement is only defined at the abstract level. Defining it at the concrete level is trivial.