×

zbMATH — the first resource for mathematics

The logic of the RAISE specification language. (English) Zbl 1104.68360
Summary: 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.

MSC:
68N15 Theory of programming languages
Software:
PVS; RAISE
PDF BibTeX XML Cite