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.
