|
Aims and scope |
 |
Projects |
| CASL Language | |
| Sublanguages | |
| Extensions | |
| |
Papers |
|
|
Approval |
 |
Extensions of CASL
HasCASL CoCASL CASL-LTL SB-CASL CSP-CASL HetCASL CASL-Refinement
Lutz Schröder, Till Mossakowski, Christian Maeder: HasCASL Language Summary.
pdf
ps
More papers
Till Mossakowski, Lutz Schröder, Markus Roggenbach, Horst Reichel:
Algebraic-coalgebraic specification in CoCASL
pdf
ps
More papers
G. Reggio, E. Astesiano, C. Choppy
CASL-LTL, a CASL extension for dynamic systems, Summary,
Version 1, 8 August 2003
ps
pdf
More papers
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.
Markus Roggenbach: CSP-CASL - A New Integration of Process Algebra
and Algebraic Specification. Submitted for publication.
pdf
ps
Till Mossakowski: HetCASL Summary.
pdf
ps
More papers
Till Mossakowski, Don Sannella, Andrzej Tarlecki:
A simple refinement language for CASL.
pdf
ps
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.
HasCASL
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. CoCASL
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).
CASL-LTL
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. SB-CASL
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. CSP-CASL
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.
HetCASL
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.
CASL-Refinement
