The role of logical interpretations in program development

Autor: Manuel A. Martins, Alexandre Madeira, Luis S. Barbosa
Jazyk: angličtina
Rok vydání: 2014
Předmět:
Zdroj: Logical Methods in Computer Science, Vol Volume 10, Issue 1 (2014)
Druh dokumentu: article
ISSN: 1860-5974
DOI: 10.2168/LMCS-10(1:1)2014
Popis: Stepwise refinement of algebraic specifications is a well known formal methodology for program development. However, traditional notions of refinement based on signature morphisms are often too rigid to capture a number of relevant transformations in the context of software design, reuse, and adaptation. This paper proposes a new approach to refinement in which signature morphisms are replaced by logical interpretations as a means to witness refinements. The approach is first presented in the context of equational logic, and later generalised to deductive systems of arbitrary dimension. This allows, for example, refining sentential into equational specifications and the latter into modal ones.
Databáze: Directory of Open Access Journals