Abstract semantics for K module composition

Codruta Girlea, Grigore Rosu

Research output: Contribution to journalArticle

Abstract

A structured K definition is easier to write, understand and debug than one single module containing the whole definition. Furthermore, modularization makes it easy to reuse work between definitions that share some principles or features. Therefore, it is useful to have a semantics for module composition operations that allows the properties of the resulting modules to be well understood at every step of the composition process. This paper presents an abstract semantics for a module system proposal for the K framework. It describes K modules and module transformations in terms of institution-based model theory introduced by Goguen and Burstall.

Original languageEnglish (US)
Pages (from-to)127-149
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Volume304
DOIs
StatePublished - Jun 10 2014

Fingerprint

Semantics
Module
Chemical analysis
Modularization
Model Theory
Reuse

Keywords

  • Abstract Modules
  • Institutions
  • K
  • Module System
  • Semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Abstract semantics for K module composition. / Girlea, Codruta; Rosu, Grigore.

In: Electronic Notes in Theoretical Computer Science, Vol. 304, 10.06.2014, p. 127-149.

Research output: Contribution to journalArticle

@article{0438bf3f43224a598b06eae63435e2ae,
title = "Abstract semantics for K module composition",
abstract = "A structured K definition is easier to write, understand and debug than one single module containing the whole definition. Furthermore, modularization makes it easy to reuse work between definitions that share some principles or features. Therefore, it is useful to have a semantics for module composition operations that allows the properties of the resulting modules to be well understood at every step of the composition process. This paper presents an abstract semantics for a module system proposal for the K framework. It describes K modules and module transformations in terms of institution-based model theory introduced by Goguen and Burstall.",
keywords = "Abstract Modules, Institutions, K, Module System, Semantics",
author = "Codruta Girlea and Grigore Rosu",
year = "2014",
month = "6",
day = "10",
doi = "10.1016/j.entcs.2014.05.007",
language = "English (US)",
volume = "304",
pages = "127--149",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Abstract semantics for K module composition

AU - Girlea, Codruta

AU - Rosu, Grigore

PY - 2014/6/10

Y1 - 2014/6/10

N2 - A structured K definition is easier to write, understand and debug than one single module containing the whole definition. Furthermore, modularization makes it easy to reuse work between definitions that share some principles or features. Therefore, it is useful to have a semantics for module composition operations that allows the properties of the resulting modules to be well understood at every step of the composition process. This paper presents an abstract semantics for a module system proposal for the K framework. It describes K modules and module transformations in terms of institution-based model theory introduced by Goguen and Burstall.

AB - A structured K definition is easier to write, understand and debug than one single module containing the whole definition. Furthermore, modularization makes it easy to reuse work between definitions that share some principles or features. Therefore, it is useful to have a semantics for module composition operations that allows the properties of the resulting modules to be well understood at every step of the composition process. This paper presents an abstract semantics for a module system proposal for the K framework. It describes K modules and module transformations in terms of institution-based model theory introduced by Goguen and Burstall.

KW - Abstract Modules

KW - Institutions

KW - K

KW - Module System

KW - Semantics

UR - http://www.scopus.com/inward/record.url?scp=84901748938&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84901748938&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2014.05.007

DO - 10.1016/j.entcs.2014.05.007

M3 - Article

AN - SCOPUS:84901748938

VL - 304

SP - 127

EP - 149

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -