How to Brew-up a Refinement Ordering

Fifty years ago there were few mathematical models of program semantics, perhaps none. Now there is probably a new one created every day. How do we do it?How should we do it? In our community we understand the utility of the refinement order, and we believe that each fresh semantics should come equipped with one. Although refinement's general principles are well understood, it is still not so easy to see just what the order should be in any particular case. Thus one of the things we should do is be clear about what the criteria really are for refinement orders.Recently invented is the Shadow Semantics for non-interference -style security of sequential programs including a refinement order. Using that as an example, I give here a rational reconstruction of how a refinement order can be “brewed-up” for a specific purpose; the aim of the exercise is to extract general lessons about how that can be done.