Authors:
The SPECTRUM specification language is axiomatic and borrows concepts both from algebraic languages (e.g. LARCH) as well as from type theoretic languages (e.g. LCF). The purpose of this report is to describe the formal semantics of the SPECTRUM kernel language. In comparison with other logics for higher order functions (e.g.~LCF family) our main contributions are a denotational semantics based on order sorted algebras for type classes, the use of non-continuous functions for specification purposes, and the identification of predicates with (strong) boolean functions in the context of a three valued logic.
Locical Framework of Spectrum, axiomatic specification language, denotational semantics, type classes
@techreport{GR94,
author = {Grosu, Radu and Regensburger, Franz},
institution = {Institut f{\"u}r Informatik, Technische-Universit{\"a}t M{\"u}nchen},
number = {TUM-I9402},
title = {The {L}ogical {F}ramework of {{\sc Spectrum}}},
year = {1994},
uri = {"http://www4.informatik.tu-muenchen.de/proj/korso/papers/frame.html" }
}