ON THE REFINEMENT OF LOGIC SPECIFICATIONS
Filomena Ferrucci, Giancarlo Nota, G. Pacini, S. OREFICE, Genny Tortora · International Journal of Software Engineering and Knowledge Engineering · 1992
Refining a specification S1 means to provide another specification S2 which contains all the information given in S1 but with more detail. In this paper, we use logical implication from lower to higher levels of logic specifications to give a definition of refinement between these levels. This guarantees that any property of the higher level is also verified at the lower one. The definition of the relation "is refinement of" is given for specifications which are general first-order theories and it is proved to be transitive. A relevant aspect is that the different levels of logic specifications are in general not immediately comparable, because they can use different vocabularies. For this reason, the concept of transcription is introduced formally in our definition. Then the particular case of Horn specifications is considered. Horn specification semantics can be given by the methodology of least models. This may suggest definitions of the concept of refinement different from the one based on logical implication from lower to higher levels. However, conceptual problems can arise depending on the kind of the refinement definition chosen. Perhaps the most interesting effect is that the property of refinement transitivity may be lost. A possible way to restore the transitivity is provided.