| Publication type: |
Article |
| Author: |
Lutz Schröder, Till Mossakowski, Andrzej Tarlecki, Piotr Hoffman, Bartek Klin |
| Title: |
Amalgamation in the semantics of CASL |
| Volume: |
331 |
| Page(s): |
215 – 247 |
| Journal: |
Theoretical Computer Science |
| Number: |
1 |
| Year published: |
2005 |
| 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.
|
| ISSN: |
0304-3975 |
| Internet: |
http://dx.doi.org/10.1016/j.tcs.2004.09.037 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/amalg.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/amalg.ps |
| Keywords: |
amalgamation CASL semantics architectural structural specification enriched |
| Status: |
Reviewed |
| Last updated: |
18. 06. 2008 |
