Casl Reference Manual

This part of the Casl Reference Manual gives a detailed summary of the syntax and intended semantics of Casl. Readers are assumed to be already familiar with the main concepts of algebraic specifications.

This part of the Casl Reference Manual defines the formal semantics of the language Casl, as informally presented in the Casl Summary (Part I). Apart from this Introduction, which is partly devoted to defining some basic notation and explaining the style of the semantics, the structure of this document is deliberately almost identical to the structure of the Casl Summary to aid cross-reference. As in the Casl Summary, Chap. 2 deals with many-sorted basic specifications, and Chap. 3 extends this by adding features for subsorted basic specifications. Chapter 4 provides structured specifications, together with specification definitions, instantiations, and views. Chapter 5 summarizes architectural and unit specifications, which, in contrast to structured specifications, prescribe the separate development of composable, reusable implementation units. Finally, Chap. 6 considers specification libraries. There are two exceptions to the structural match between this document and the Casl Summary. One is in Chap. 4, where the subsections of Sect. 4.1 define many concepts and notations underlying the semantics of structured specifications that were not mentioned in the Casl Summary. The other is in Chap. 5, where Sect. 5.6 presents a more precise analysis of the constructs considered in Sects. 5.2–5.5.

This part of the Casl Reference Manual provides proof calculi for the various levels of Casl specifications. It should be read together with the the Casl semantics (Part III).

This part of the Casl reference manual describes a library of elementary specifications called the Basic Datatypes. This library has been developed with two main purposes in mind: on the one hand, it provides the user with a handy set of off-the-shelf specifications to be used as building blocks in the same way as library functions in a programming language, thus avoiding continuous reinvention of the wheel. On the other hand, it serves as a large reservoir of example specifications that illustrate both the use of Casl at the level of basic and structured specifications. The specification methodology behind the Basic Datatypes is described in [57].