Gutiérrez Gil, R.; Meseguer, J.; Rocha, C. (2015). Order-Sorted Equality Enrichments Modulo Axioms. Science of Computer Programming. 99:235-261. https://doi.org/10.1016/j.scico.2014.07.003
Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/64704
Título:
|
Order-Sorted Equality Enrichments Modulo Axioms
|
Autor:
|
Gutiérrez Gil, Raúl
Meseguer, Jose
Rocha, Camilo
|
Entidad UPV:
|
Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
|
Fecha difusión:
|
|
Resumen:
|
Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications ...[+]
Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation epsilon bar right arrow epsilon(similar to) that extends an algebraic specification epsilon to a specification epsilon(similar to) having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications epsilon that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation epsilon bar right arrow epsilon(similar to) preserves all the just-mentioned properties of epsilon. The transformation has been automated in Maude using reflection and is used as a component in many Maude formal tools. (C) 2014 Elsevier B.V. All rights reserved.
[-]
|
Palabras clave:
|
Equality predicate
,
Order-sorted equational logic modulo
,
Axioms
,
Algebraic specifications
,
Initial algebra semantics
,
Maude
|
Derechos de uso:
|
Reserva de todos los derechos
|
Fuente:
|
Science of Computer Programming. (issn:
0167-6423
)
|
DOI:
|
10.1016/j.scico.2014.07.003
|
Editorial:
|
Elsevier
|
Versión del editor:
|
http://dx.doi.org/10.1016/j.scico.2014.07.003
|
Código del Proyecto:
|
info:eu-repo/grantAgreement/NSF//1319109/US/TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude/
...[+]
info:eu-repo/grantAgreement/NSF//1319109/US/TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude/
info:eu-repo/grantAgreement/NSF//0905584/US/TC: Medium: Collaborative Research: Rewriting Logic Foundations for Verification and Programming of Next-Generation Trustworthy Web-Based Systems/
info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/
info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/
info:eu-repo/grantAgreement/MINECO//JCI-2012-13528/ES/JCI-2012-13528/
[-]
|
Agradecimientos:
|
This work has been supported in part by NSF Grants CCF 09-05584 and CNS 13-19109, the EU (FEDER) and the Spanish MINECO under Grants TIN 2010-21062-C02 and TIN 2013-45732-C4-1-P, and by the Generalitat Valenciana, ref. ...[+]
This work has been supported in part by NSF Grants CCF 09-05584 and CNS 13-19109, the EU (FEDER) and the Spanish MINECO under Grants TIN 2010-21062-C02 and TIN 2013-45732-C4-1-P, and by the Generalitat Valenciana, ref. PROMETEO/2011/052. Raul Gutierrez is also partially supported by a Juan de la Cierva Fellowship from the Spanish MINECO, ref. JCI-2012-13528.
[-]
|
Tipo:
|
Artículo
|