Abstract: |
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. |