

Extensions of CASL
HasCASL
CoCASL
CASLLTL
SBCASL
CSPCASL
HetCASL
CASLRefinement
The development of programs in modern functional languages such as
Haskell calls for a widespectrum 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 settheoretic 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 lightweight 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
observerindexed 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:
Algebraiccoalgebraic 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. CASLLTL 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 logicalgebraic 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
CASLLTL, a CASL extension for dynamic systems, Summary,
Version 1, 8 August 2003
ps
pdf
More papers
SBCASL stands for "Statebased CASL", it is based on the
stateasalgebra 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.
SBCASL uses CASL for the specification of the static part of a state,
and the structuring mechanisms of CASL are used for structuring
SBCASL specifications.
Hubert Baumeister, Alexandre Zamulin.
StateBased Extension of CASL,
Integrated Formal Methods (Second
International Conference, IFM 2000, Dagstuhl Castle, Germany, November
2000, Proceedings), LNCS, vol. 1945, pp. 324.
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.
CSPCASL 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 subsorting. Technically, this integration involves the
development of a new cocalled datalogic formulated as an
institution. This datalogic 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: CSPCASL  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 CASLRefinement is not finished yet.
Till Mossakowski, Don Sannella, Andrzej Tarlecki:
A simple refinement language for CASL.
pdf
ps
