Abstract
This paper 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.
Keywords
Cite this article
@article{cai-1318-2003-3-4,
author = {Chris George and Anne E. Haxthausen},
title = {The Logic of the RAISE},
journal = {Computing and Informatics},
volume = {22},
number = {3-4},
pages = {323--350},
year = {2003},
issn = {1335-9150},
url = {https://cai.type.sk/content/2003/3-4/the-logic-of-the-raise/}
}
TY - JOUR AU - Chris George AU - Anne E. Haxthausen TI - The Logic of the RAISE JO - Computing and Informatics VL - 22 IS - 3-4 SP - 323 EP - 350 PY - 2003 SN - 1335-9150 UR - https://cai.type.sk/content/2003/3-4/the-logic-of-the-raise/ KW - Formal methods KW - logics KW - RAISE ER -
George, C., & Haxthausen, A. E. (2003). The Logic of the RAISE. Computing and Informatics, 22(3-4), 323–350. https://cai.type.sk/content/2003/3-4/the-logic-of-the-raise/