DFG Project HasCASL

HasCASL: Algebraic Specification + Functional Programming = Environment for Formal Software Development

The algebraic specification language CASL (Common Algebraic Specification Langage) has recently been developed by the Common Framework Initiative (CoFI) as the centerpiece of an internationally standardized family of specification languages. It is the aim of this project to develop an extension of CASL that establishes a connection with the functional programming language Haskell. To this end, CASL has been extended by features of higher order logic w.r.t. syntax, formal semantics and tool support; Haskell corresponds to an executable sublanguage of the extended language. Thus, an environment is created for the specification and formal implementation of software that allows the coherent development of formal specifications and executable functional programs in a common framework. HasCASL has been adopted as an official CASL extension by IFIP WG 1.3 in 2004.

The HasCASL tools are being developed as a part of the Bremen heterogeneous tool set Hets. The implementation language is Haskell. Presently, Hets includes a parser and a static analysis tool for HasCASL, as well as prototypic proof support and a translation of executable specifications into Haskell.

Material on HasCASL

The full language definition is contained in the following extension of the CASL Summary:

L. Schröder, T. Mossakowski and C. Maeder: HasCASL - Integrated functional specification and programming. Language summary. [Postscript][PDF]

L. Schröder and T. Mossakowski: HasCASL - Integrated Higher-Order Specification and Program Development [PDF]

A brief overview of the language design can be found in

Lutz Schröder, Higher order and reactive algebraic specification and development (summary of papers constituting a cumulative habilitation thesis) [PDF] [PS]

There is also a full list of HasCASL publications from Bremen, including papers on the semantic foundations, case studies, and monad-based generic computational logics with applications to the modelling of Java-style exceptions.

Contact: Lutz Schröder.