| Abstract: |
In this work, we consider various specification specification languages and their relation to CASL, the recently developed Common Algebraic Specification Language. In particular, we consider the languages Larch, OBJ3, ACT, ASF, and HEP-theories. We also consider various sublanguages of CASL that more or less directly correspond to these. All these languages are translated to an appropriate sublanguage of CASL. The translation considers only the level of specification in-the-small: the logics underlying the languages are formalized as institutions, and representations among the institutions are developed. The institution representations concern on one hand the translation of the CASL institution (and some of its subinstitutions) to simpler subinstitutions. Given a theorem proving tool for such a simpler subinstitutions, with the help of such a representation, it can also be used for the more complex institution. Thus, first-order theorem provers or conditional term rewriting tools become usable for CASL. On the other hand, we set up institution representations between the underlying institution of any of the abovementioned specification languages and an appropriate subinstitution of CASL. This allows to take libraries and case studies that have been developed for other languages and re-use them in CASL. |
