TY - JOUR
T1 - CASL, the Common Algebraic Specification Language: Semantics and Proof Theory
AU - Mossakowski, Till
AU - Haxthausen, Anne Elisabeth
AU - Sannella, Donald
AU - Tarlecki, Andrzej
PY - 2003
Y1 - 2003
N2 - 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 structure of implementations). We describe an simplified version of the CASL syntax, semantics and proof calculus at 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.
AB - 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 structure of implementations). We describe an simplified version of the CASL syntax, semantics and proof calculus at 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.
M3 - Journal article
SN - 1335-9150
VL - 22
SP - 285
EP - 321
JO - Computing and Informatics
JF - Computing and Informatics
IS - 3-4
ER -