A theory of mixin modules: algebraic laws and reduction semantics Partially supported by Murst (Tecniche formali per la specifica, lʼanalisi, la verifica, la sintesi e la trasformazione di sistemi software) and CNR (Formalismi per la specifica e la descrizione di sistemi ad oggetti).
ANCONA, DAVIDE; ZUCCA, ELENA; ANCONA DAVIDE; Dipartimento di Informatica e Scienze dellʼInformazione; ZUCCA ELENA; Dipartimento di Informatica e Scienze dellʼInformazione
Журнал:
Mathematical Structures in Computer Science
Дата:
2002
Аннотация:
Mixins are modules that may contain deferred components, that is, components not defined in the module itself; moreover, in contrast to parameterised modules (like ML functors), they can be mutually dependent and allow their definitions to be overridden. In a preceding paper we defined a syntax and denotational semantics of a kernel language of mixin modules. Here, we take instead an axiomatic approach, giving a set of algebraic laws expressing the expected properties of a small set of primitive operators on mixins. Interpreting axioms as rewriting rules, we get a reduction semantics for the language and prove the existence of normal forms. Moreover, we show that the model defined in the earlier paper satisfies the given axiomatisation.
461.3Кб