The CoFI-Language Group Home Page
- Aims and scope
- Projects
CASL Language
- Papers
- Approval

Extensions of CASL



The development of programs in modern functional languages such as Haskell calls for a wide-spectrum specification formalism that supports the type system of such languages, in particular higher order types, type constructors, and polymorphism, and that contains a functional language as an executable subset in order to facilitate rapid prototyping. We lay out the design of HasCASL, a higher order extension of CASL that is geared towards precisely this purpose. Its semantics is tuned to allow program development by specification refinement, while at the same time staying close to the set-theoretic semantics of first order CASL. The number of primitive concepts in the logic has been kept as small as possible; advanced concepts, in particular general recursion, can be formulated within the language itself. This document provides a detailed definition of the HasCASL syntax and an informal description of the semantics, building on the existing CASL Summary.

Lutz Schröder, Till Mossakowski, Christian Maeder: HasCASL Language Summary. pdf ps   More papers


CoCASL is a light-weight but expressive coalgebraic extension of the algebraic specification language CASL. CoCASL allows the nested combination of algebraic datatypes and coalgebraic process types. Moreover, it provides syntactic sugar for an observer-indexed modal logic that allows e.g. expressing fairness properties. This logic includes a generic definition of modal operators for observers with structured equational result types. We prove existence of final models for specifications in a format that allows the use of certain initial datatypes, as well as modal axioms. The use of CoCASL is illustrated by specifications of the process algebras CSP and CCS.

Till Mossakowski, Lutz Schröder, Markus Roggenbach, Horst Reichel: Algebraic-coalgebraic specification in CoCASL pdf ps  More papers


CASL, the basic language developed within CoFI, the Common Framework Initiative for algebraic specification and development, cannot be used for specifying requirements and design for dynamic software systems. CASL-LTL is an extension to overcome this limit, allowing to specify dynamic system by modelling them by means of labelled transition systems and by expressing their properties with temporal formulae. It is based on LTL a logic-algebraic formalism for the specification of concurrent systems mainly devoleped by E.Astesiano and G. Reggio (see more papers section).

G. Reggio, E. Astesiano, C. Choppy CASL-LTL, a CASL extension for dynamic systems, Summary, Version 1, 8 August 2003 ps pdf   More papers


SB-CASL stands for "State-based CASL", it is based on the state-as-algebra approach and allows specifications of complex dynamic systems in the style of Z and Gurevich's ASMs. A dynamic system is defined by a set of states and a set of operations/procedures for transforming one state into another. A state consists of a fixed static part and a varying part. The static part is the same for all states of a dynamic system and is given by a CASL specification. The varying part includes dynamic sorts/functions/predicates. The operations and procedures update the variable part of the state and are given by pre- and postconditions and/or dynamic equations. SB-CASL uses CASL for the specification of the static part of a state, and the structuring mechanisms of CASL are used for structuring SB-CASL specifications.

Hubert Baumeister, Alexandre Zamulin. State-Based Extension of CASL, Integrated Formal Methods (Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 2000, Proceedings), LNCS, vol. 1945, pp. 3-24. ps.gz

A corresponding adaptation of the CASL Summary, as well as a document describing the semantics in more detail, is in preparation, and is to be made available at a later date.


CSP-CASL is a combination of the process algebra CSP and the algebraic specification language CASL. Its novel aspects include the combination of denotational semantics in the process part and, in particular, loose semantics for the data types covering both concepts partiality and sub-sorting. Technically, this integration involves the development of a new co-called data-logic formulated as an institution. This data-logic serves as a link between the institution underlying CASL and the alphabet of communications necessary for the CSP semantics. Besides being generic in the various denotational CSP semantics, this construction leads also to an appropriate notion of refinement with clear relations to both data refinement in CASL and process refinement in CSP.

Markus Roggenbach: CSP-CASL - A New Integration of Process Algebra and Algebraic Specification. Submitted for publication. pdf ps


Heterogeneous CASL (HetCASL) allows mixing specifications written in different logics (using translations between the logics). It extends CASL only at the level of structuring constructs, by adding constructs for choosing the logic and translating specifications among logics. HetCASL is needed when combining specifications written in CASL with specifications written in its sublanguages and extensions. HetCASL also allows the integration of logics that are completely different from the CASL logic.

Till Mossakowski: HetCASL Summary. pdf ps   More papers


CASL is extended with constructs for expressing refinements between structured, unit and architectural specifications. The relation to programming languages is also addressed. The design of CASL-Refinement is not finished yet.

Till Mossakowski, Don Sannella, Andrzej Tarlecki: A simple refinement language for CASL. pdf ps

Back to CoFI-Language Home Page