Creating a HasCASL Library

The effective use of a speci¿cation language depends on the availability of prede¿ned speci¿cations. Although the CASL speci¿cation has such a library, that is not the case of the HasCASL language, one of the CASL?s extensions. Here we start to specify such a library to the HasCASL language, based on the Prelude library of the Haskel l programming language. When completed this approach would create a library that, after re¿nements, should lead to reusable speci¿cations for real Haskel l programs. This technical report discusses the speci¿cation and veri¿cation of a kernel library to the HasCASL language.

2009