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.
In corso di stampa
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).
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11388/170365
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact