Semantics of the Specification Language ACT ONE

Abstract

In this chapter we present the semantics of the algebraic specification language ACT ONE which was introduced in the last chapter. The semantics is defined formally on two levels: The first level is that of parameterized specifications and the second that of free functors associated with parameterized specifications in the sense of Chapter 7. Given an ACT ONE definition we define in the first level the corresponding parameterized specifications PSPEC = (FSPEC,TSPEC), where FSPEC is the formal parameter and TSPEC the target specification. Note that, although PSPEC was viewed as a syntactical object in Chapters 7 and 8, is it now the first level of semantics of an ACT ONE definition. The definition has now to be considered as the syntactical level. The semantics of PSPEC in the sense of Chapter 7 are all free functors F:Cat(FSPEC) → Cat(TSPEC). In this chapter we represent the semantics by only one free functor F because all other ones are natural isomorphic to F. Since PSPEC = (FSPEC,TSPEC) was already the first level of semantics w.r.t. the given ACT ONE definition, the parameterized data type PDAT = (FSPEC,TSPEC,F) is the second level of semantics w.r.t. the ACT ONE definition.