Preorder-Constrained Simulations for Program Refinement with Effects

We propose a notion of preorder-constrained simulation. It is parameterised by a preorder (“observation preorder”) on traces, so that it can uniformly characterise quantitative notions of program refinement for different effects, such as exception, nondeterminism and I/O. Preorder-constrained simulation is additionally parameterised by a positive number (“look-ahead bound”), and forms a generative spectrum governed by the look-ahead bound. We analyse the complexity of determining preorder-constrained similarity, and show that preorder-constrained simulation can be enhanced by the so-called up-to technique.