Generic Tools via General Refinement

Tools have become essential in the formal model-driven development of software but are very time consuming to build and often restricted to a particular semantic interpretation of a particular syntax. This is regrettable since there is large amount in common between tools, even if they do "implement" different syntaxes and different semantics. We propose splitting tools into front-and back-ends where an operational semantics acts as the link between the two. We will not have much to say about the front-end and the link in this paper since it is theoretically straightforward. Instead, we concentrate on the second part and provide a well-motivated, general, mathematical framework to form the underlying theory that gives great flexibility to the back-end of a tool which is concerned with developing software via stepwise refinement. From a general model of refinement between two entities, where the refinement is parameterised on contexts and observations, we build logical theories which have refinement as implication. Further, we consider what can be expected of a guarantee concerning the behaviour of an implementation relative to a specification. Then by fixing the contexts and observations in suitable ways, and so getting particular, special models of refinement, we give a formal interpretation of a guarantee. To this we add theory morphisms between special models, where a theory morphism can change the contexts and observations we can make in controlled and useful ways, mainly by preserving a refinement relation between entities even as we change them. We show how the generality brought about by the parameterisation allows an example from the literature, which seems formally not to be a refinement, to be captured as a refinement, in accordance with our intuitions about the example. In this way we show the flexibility of our theory for a refinement tool back-end. From this it follows that the effort put into building a tool based on our theory will be well-spent-a single tool should be parameterised (just as our theory is) to deal with the many different notions of refinement found in the literature. Thus we make a contribution to the problem of ensuring correctness and dependability of software using formal methods and tools of modelling, design, verification and validation.