This paper studies the structure of semantic theories over modular computational systems and applies the algebraic Theory of Institutions to provide a logical representation of such theories. A modular semantic theory is here defined by a cluster of semantic theories, each for a single program’s module, and by a set of relations connecting models of different semantic theories. A semantic theory of a single module is provided in terms of the set of Σ-models mapped from the category Th of Σ-theories and generating a hierarchy of structures from an abstract model to a concrete model of data. The collection of abstract models representing different modules of a program is formalised as the category of institutions INS, where theory morphisms express refinements, integrations, and compositions between couples of modules. Finally, it is required that a morphism in INS at any level occurs iff the same morphism occurs at the lower level alongside the Th hierarchy.
The Logical Structure of Modular Semantic Theories of Software Systems / Angius, Nicola; Stefaneas, Petros. - In: JOURNAL OF LOGIC AND COMPUTATION. - ISSN 0955-792X. - (In corso di stampa).
The Logical Structure of Modular Semantic Theories of Software Systems
ANGIUS, Nicola;
In corso di stampa
Abstract
This paper studies the structure of semantic theories over modular computational systems and applies the algebraic Theory of Institutions to provide a logical representation of such theories. A modular semantic theory is here defined by a cluster of semantic theories, each for a single program’s module, and by a set of relations connecting models of different semantic theories. A semantic theory of a single module is provided in terms of the set of Σ-models mapped from the category Th of Σ-theories and generating a hierarchy of structures from an abstract model to a concrete model of data. The collection of abstract models representing different modules of a program is formalised as the category of institutions INS, where theory morphisms express refinements, integrations, and compositions between couples of modules. Finally, it is required that a morphism in INS at any level occurs iff the same morphism occurs at the lower level alongside the Th hierarchy.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.