The Logic of the RAISE Specification Language

    Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

    Abstract

    This chapter describes the logic of the RAISE Specification Language, RSL. It explains the particular logic chosen for RAISE, and motivates this choice as suitable for a wide spectrum language to be used for designs as well as initial specifications, and supporting imperative and concurrent specifications as well as applicative sequential ones. It also describes the logical definition of RSL, its axiomatic semantics, as well as the proof system for carrying out proofs. Finally, a case study illustrates specification and verification methods in RAISE.
    Original languageEnglish
    Title of host publicationLogics of Specification Languages
    EditorsDines Bjørner, Martin C. Henson
    PublisherSpringer
    Publication date2008
    ISBN (Print)978-3-540-74106-0
    Publication statusPublished - 2008
    SeriesMonographs in Theoretical Computer Science. An EATCS Series
    NumberXXII

    Keywords

    • RAISE

    Fingerprint Dive into the research topics of 'The Logic of the RAISE Specification Language'. Together they form a unique fingerprint.

    Cite this