Algebraic compilers provide a powerful and convenient mechanism for specifying language translators. With each source language operation one associates a computation for constructing its target language image; these associated computations, called derived operations, are expressed in terms of operations from the target language. Sometimes the target language is not powerful enough to specify the required translation and one may then need to extend the target language algebras with more computationally expressive operations or elements. A better solution is to package these extensions in a specification language which can be composed with the target language to ensure that all operations and elements needed or desired for performing the translation are provided. In the example in this paper, we show how imperative and functional specification languages can be composed with a target language to implement a temporal logic model checker as an algebraic compiler and show how specification languages can be seen as components to be combined with a source and target language to generate an algebraic compiler.
|Original language||English (US)|
|Number of pages||35|
|Journal||Theoretical Computer Science|
|State||Published - Jan 6 2003|
|Event||Algebraic Methodology and Software Technology (AMAST 2000) - Iowa City, IO, United States|
Duration: May 20 2000 → May 27 2000
Bibliographical noteFunding Information:
We would like to thank the anonymous reviewers for their helpful suggestions in improving this paper and Microsoft Research for funding this research.
- Algebraic compiler
- Specification languages