New study notes

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear friends,

two new semantics study notes have just been installed:

Note S-11
           Semantics of Architectural Specifications in CASL

by Lutz Schröder, Till Mossakowski, Andrzej Tarlecki, Bartek Klin
   and Piotr Hoffman.
Available at:
http://www.brics.dk/Projects/CoFI/Notes/S-11/
ftp://ftp.brics.dk/Projects/CoFI/Notes/S-11/

Note S-12
           Extending development graphs with hiding

by Till Mossakowski, Serge Autexier and Dieter Hutter.
Available at:
http://www.brics.dk/Projects/CoFI/Notes/S-12/
ftp://ftp.brics.dk/Projects/CoFI/Notes/S-12/


Abstract of S-11:
We present a semantics for architectural specifications in CASL, including an
extended static analysis compatible with model-theoretic requirements.  The
main obstacle here is the lack of amalgamation for CASL models.  To
circumvent this problem, we extend the CASL logic by introducing enriched
signatures, where subsort embeddings form a category rather than just a
preorder.  The extended model functor has amalgamation, which makes it
possible to express the amalgamability conditions in the semantic rules in
static terms.  Using these concepts, we develop the semantics at various
levels in an institution-independent fashion.  Concretizing to the CASL
institution, we discuss a calculus for discharging the static amalgamation
conditions.  These are in general undecidable, but can be dealt with by
approximative algorithms in all practically relevant cases.

Abstract of S-12:
Development graphs are a tool for dealing with structured specifications in a
way easing management of change and reusing proofs.  In this work, we extend
development graphs with hiding.  Hiding is a particularly difficult to
realize operation, since it does not admit such a good decomposition of the
involved specifications as other structuring operations do.  We develop both
a semantics and proof rules for development graphs with hiding.  The rules
are proven to be sound, and also complete relative to an oracle for
conservative extensions.  We also show that an absolute complete set of rules
cannot exist.  The whole framework is developed in a way independent of the
underlying logical system.

Greetings,
Till
-----------------------------------------------------------------------------
Till Mossakowski                Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            till@informatik.uni-bremen.de           
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------