CASL --- the Common Algebraic Specification Language

Till Mossakowski, Anne E. Haxthausen, Donald Sannella, Andrezj Tarlecki

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract / Description of output

CASL is an expressive specification language that has been designed to supersede many existing algebraic specification languages and provide a standard. CASL consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications; the latter are used to prescribe the modular structure of implementations. We describe a simplified version of the CASL syntax, semantics and proof calculus for each of these three layers and state the corresponding soundness and completeness theorems. The layers are orthogonal in the sense that the semantics of a given layer uses that of the previous layer as a black box, and similarly for the proof calculi. In particular, this means that CASL can easily be adapted to other logical systems. We conclude with a detailed example specification of a warehouse, which serves to illustrate the application of both CASL and the proof calculi for the various layers.
Original languageEnglish
Title of host publicationLogics of Specification Languages
EditorsDines Bjørner, Martin C. Henson
PublisherSpringer
Pages241-298
Number of pages58
ISBN (Electronic)978-3-540-74107-7
ISBN (Print)978-3-540-74106-0
DOIs
Publication statusPublished - 2008

Publication series

NameMonographs in Theoretical Computer Science. An EATCS Series
PublisherSpringer Berlin Heidelberg
ISSN (Print)1431-2654

Fingerprint

Dive into the research topics of 'CASL --- the Common Algebraic Specification Language'. Together they form a unique fingerprint.

Cite this