Project

HasCASL

HasCASL

  • Duration:

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.

Sponsors

Deutsche Forschungsgemeinschaft (DFG)

KR 1191/7-2

Deutsche Forschungsgemeinschaft (DFG)

Publications about the project

In: Theoretical Computer Science 410 12-13 Pages 1217-1260 Elsevier 2009.

To the publication

In: Logical Methods in Computer Science (LMCS) 4 4:17 Pages 1-27 2008.

To the publication

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz