%0 Journal Article %1 SchroderEA04 %A Schröder, Lutz %A Mossakowski, Till %A Tarlecki, Andrzej %A Hoffman, Piotr %A Klin, Bartek %D 2005 %J Theoretical Computer Science %K CASL amalgamation architectural enriched semantics specification structural %N 1 %P 215-247 %T Amalgamation in the semantics of CASL %U http://dx.doi.org/10.1016/j.tcs.2004.09.037 %V 331 %X 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 satisfies the amalgamation property as well as its converse, 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. Moreover, amalgamation for enriched CASL means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for CASL.

@article{SchroderEA04, abstract = {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 satisfies the amalgamation property as well as its converse, 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. Moreover, amalgamation for enriched CASL means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for CASL. }, added-at = {2016-08-05T15:59:03.000+0200}, author = {Schr{\"o}der, Lutz and Mossakowski, Till and Tarlecki, Andrzej and Hoffman, Piotr and Klin, Bartek}, biburl = {https://www.bibsonomy.org/bibtex/2ed2ab415a6d90a7bec5b5eb64ae2c853/tillmo}, interhash = {035f44c0dc3391f97acda457588ac07b}, intrahash = {ed2ab415a6d90a7bec5b5eb64ae2c853}, issn = {0304-3975}, journal = {Theoretical Computer Science}, keywords = {CASL amalgamation architectural enriched semantics specification structural}, number = 1, pages = {215-247}, pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/amalg.pdf}, psurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/amalg.ps}, status = {Reviewed}, timestamp = {2016-08-05T15:59:03.000+0200}, title = {Amalgamation in the semantics of {CASL}}, url = {http://dx.doi.org/10.1016/j.tcs.2004.09.037}, volume = 331, year = 2005 }