An Institution for Imperative RSL Specifications

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

1 Downloads (Pure)


The RAISE Specification Language (RSL) is a wide-spectrum specification language having a very complex semantics. This paper defines an institution for an imperative subset RSLI of RSL such that this subset can be given a much simpler semantics in terms of that institution. The subset allows model-oriented type definitions, declaration of state variables, axiomatic specification of values (including functions), and explicit function definitions. Functions may be imperative. The semantics of an RSLI specification is defined to be the loose semantics of a theory presentation consisting of a signature Σ and a set of sentences E that can easily be derived from the specification.
Original languageEnglish
Title of host publicationSpecification, Algebra, and Software : Essays Dedicated to Kokichi Futatsugi
Publication date2014
ISBN (Print)978-3-642-54623-5
ISBN (Electronic)978-3-642-54624-2
Publication statusPublished - 2014
SeriesLecture Notes in Computer Science

Fingerprint Dive into the research topics of 'An Institution for Imperative RSL Specifications'. Together they form a unique fingerprint.

Cite this