Specification languages in algebraic compilers

DOI10.1016/S0304-3975(02)00367-5MaRDI QIDQ1853753zbMATH OpenOpenAlexWikidataFDO

Publication date 22 January 2003

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(02)00367-5

algebraic compiler specification languages

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

Cites work

Cited in

(4)

This page was built for publication: Specification languages in algebraic compilers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853753)