An Institution for Imperative RSL Specifications

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

1 Downloads (Pure)

Abstract

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
PublisherSpringer
Publication date2014
Pages441-464
ISBN (Print)978-3-642-54623-5
ISBN (Electronic)978-3-642-54624-2
DOIs
Publication statusPublished - 2014
SeriesLecture Notes in Computer Science
Volume8373
ISSN0302-9743

Fingerprint

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

Cite this