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 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.
Poza referatem na tym pierwszym po feriach spotkaniu będziemy ustalać plan referatów na drugi semestr, zachęcam do zgłaszania tematów i terminów, osobiście na seminarium lub zdalnie emailem do mnie (P.Czarnika).
You are not logged in |
