Andrzej Tarlecki

Another Old Story: Compositional Property-oriented Semantics for
Structured Specifications

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 one-step 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 not "absent-minded", i.e., do not loose
axioms of flat specifications. We sketch an example to show that by
excluding deduction of some axioms in flat specifications we may offer
a stronger rule for natural specification-building operation so that
for some specifications the resulting semantics is stronger than the
standard one.