Publikation
Creating a HasCASL library
Glauber Cabral; Christian Maeder; Till Mossakowski; Lutz Schröder
In: Jonathan Aldrich; Ricardo Massa (Hrsg.). 14th Brazilian Symposium on Programming Languages. Brazilian Symposium on Programming Languages (SBLP-10), located at Brazilian Conference on Software: Theory and Practice, September 27 - October 1, Salvador-Bahia, Brazil, 9/2010.
Zusammenfassung
A prerequisite for the practical use of a specification language is the existence of a set of predefined specifications. Although the Common Algebraic Specification Language (CASL) has a library with such predefined specifications, its higher order extension, named HASCASL, still lacks a library with basic higher order data types and functions. In this paper, we describe the specification and verification of a library for the HASCASL language. Our library covers a subset of the Haskell Prelude library, including data types and classes representing Booleans, lists, characters, strings, equality, and ordering functions. We use the Heterogeneous Tool Set (HETS) for parsing specifications, generating proof obligations, and translating between the HASCASL and HOL languages. To discharge the arising proof obligations, we use the Isabelle/HOL interactive theorem prover.