Talk "Compositional Property-oriented Semantics for Structured Specifications. Another Old Story (with a Few New Twists) "

by Andrzej Tarlecki

Sat, 03 September 2011 at 03:00 pm in Winchester, United Kingdom

Abstract: Working in an arbitrary institution, we discuss property-oriented semantics of specifications built using some collection of specification-building operations. As a typical example we consider the structured specifications built from flat specifications using union, translation and hiding. For such specifications we have the standard compositional proof system, which determines the standard property-oriented semantics assigning a theory to each structured specification. It is not complete (unless the underlying logic has interpolation and enjoys some other technical properties) but otherwise it is "as good as can be expected". In particular, it is sound, monotone (and hence compositional) and closed complete. The last property means that the semantics (and the corresponding proof system) allows us to deduce all true consequences for specifications built by applying any specification-building operation to argument specifications, assuming that there is no discrepancy between the classes of models of the argument specifications and the classes of models of their respective property-oriented meanings. This is a strong property which was believed to ensure that the semantics is "as strong as possible" without loosing soundness or compositionality. We question this claim and show that it holds assuming in addition that the semantics considered are theory-oriented, i.e., the sets of properties assigned to specifications are closed under consequence, as well as non-absent-minded, i.e., no axioms from flat specifications are omitted as properties. We sketch examples to show that neither of these requirements may be dropped. We generalise this study to the context of entailment systems, and show similar results and counterexamples.