|  |
| Title:
|
The Logic of the RAISE Specification Language |
| Type:
|
Book chapterBook chapter |
| Participant(s):
|
Forfatter:
George, Chris
UNU/IIST
Technical University of Denmark
Email:
|
| 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. |
| Published:
|
part of: Logics of Specification Languages (ISBN: 978-3-540-74106-0), 2008, Springer, |
|
|