Title: Algebraic explanation of Hoare's notion of refinement

Abstract:

Refinement is a notion in software engineering.  One "refines" data or
programs.  Taking the idea from Hoare, we formulate program refinement
as follows.  We first define a syntax for programs.  We then develop a
functorial semantics for that; so an interpretation is a functor.  We
wish to compare two interpretations and show that one is a refinement
of the other.  For that purpose, we need an order in homsets, so, we
develope the functorial semantics with locally ordered categories and
locally ordered functors, rather than mere categories and functors.
The refinement relation is then an existence of lax transformation
between the interpretation locally ordered functors.

So, we show how these mathematical machinary is used in formulating
refinement.  Especially, the "extensibility" phenomenon Hoare
mentioned about refinement in his unpublished draft is explained by
enriched adjunction and we can say that such extension is possible
whenever the language construct can be described as algebraic
structure on LocOrd_l, defined in the next paragraph.  This means our
theory covers a number of language constructs but, to make the talk
more concrete, we put a nondeterministic imperative language with at
most countable number of branches.  In this language, it is easy to
encode "if" statements and "while" statements, so we regard it is an
appropriate model to argue about imperative languages.  We also
mention about the language used in the work by Hoare, He and Sanders,
where one wishes to model the iteration by greatest fixpoints.  That
language cannot be modelled by relation algebras, but it can be
described by algebraic structure on LocOrd_l.

Then we go to mathematical background of our work.  The category of
locally ordered categories and locally ordered functors has monoidal
structure given by so called Gray tensor.  It is not symmetric but it
is biclosed.  Moreover, that category is enriched over itself, by
considering the category of locally ordered functors and lax
transformations.  We call the enriched category LocOrd_l, l for lax
transformation.  We show how countableary LocOrd_l-algebraic
structures on LocOrd_l is defined in detail and show the definition of
algebraic structure describing the structure of our language.  We need
countable arity in order to model the countable nondeterminism.