The role of logical interpretations in program development

DOI10.2168/LMCS-10(1:1)2014MaRDI QIDQ2871226zbMATH OpenFDO

Authors Manuel A. Martins, Alexandre Madeira, L. S. Barbosa

Publication date 22 January 2014

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1311.7090

zbMATH Keywords

algebraic specificationdeductive systemlogical interpretationrefinement

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Abstract: 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.

Recommendations

• Refinement by Interpretation in a General Setting
• A coalgebraic perspective on logical interpretations
• Observational refinement process
• A logic for schema-based program development
• A refinement calculus for logic programs

Cited in

(3)

• Behavioral equivalence of hidden k-logics: an abstract algebraic approach
• A coalgebraic perspective on logical interpretations
• Observational refinement process

Describes a project that uses

Uses Software

• CASL
• OBJ3
• CafeOBJ
• Maude
• Hets
• LATIN

This page was built for publication: The role of logical interpretations in program development

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2871226)