TY - JOUR
T1 - On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
AU - Durán, Francisco
AU - Meseguer, José
N1 - Funding Information:
We thank the referees for their careful reading of a previous version and their very helpful suggestions to improve the exposition. We also thank Salvador Lucas and Camilo Rocha for their help discharging some of the proof obligations encountered when preparing the examples in Section 5, and Santiago Escobar for very fruitful discussions on the use of the narrowing library in Maude as a component of the CRC and ChC tools. F. Durán was supported by Spanish Research Projects TIN2008-03107 and P07-TIC-03184. J. Meseguer was partially supported by NSF Grants CCF-0905584, CNS-07-16038, CNS-09-04749, and CNS-08-34709.
PY - 2012/10
Y1 - 2012/10
N2 - In the effort to bring rewriting-based methods into contact with practical applications both in programing and in formal verification, there is a tension between: (i) expressiveness and generality - so that a wide range of applications can be expressed easily and naturally - and (ii) support for formal verification, which is harder to get for general and expressive specifications. This paper answers the challenge of successfully negotiating the tension between goals (i) and (ii) for a wide class of Maude specifications, namely: (a) equational order-sorted conditional specifications (Σ,E∪A), corresponding to functional programs modulo axioms such as associativity and/or commutativity and/or identity axioms and (b) order-sorted conditional rewrite theories R=(Σ,E∪A,R,φ), corresponding to concurrent programs modulo axioms A. For Maude functional programs the key formal property checked is the Church-Rosser property. For concurrent declarative programs in rewriting logic, the key property checked is the coherence between rules and equations modulo the axioms A. Such properties are essential, both for executability purposes and as a basis for verifying many other properties, such as, for example, proving inductive theorems of a functional program, or correct model checking of temporal logic properties for a concurrent program. This paper develops the mathematical foundations on which the checking of these properties (or ground versions of them) is based, presents two tools, the Church-Rosser Checker (CRC) and the Coherence Checker (ChC) supporting the verification of these properties, and illustrates with examples a methodology to establish such properties using the proof obligations returned by the tools.
AB - In the effort to bring rewriting-based methods into contact with practical applications both in programing and in formal verification, there is a tension between: (i) expressiveness and generality - so that a wide range of applications can be expressed easily and naturally - and (ii) support for formal verification, which is harder to get for general and expressive specifications. This paper answers the challenge of successfully negotiating the tension between goals (i) and (ii) for a wide class of Maude specifications, namely: (a) equational order-sorted conditional specifications (Σ,E∪A), corresponding to functional programs modulo axioms such as associativity and/or commutativity and/or identity axioms and (b) order-sorted conditional rewrite theories R=(Σ,E∪A,R,φ), corresponding to concurrent programs modulo axioms A. For Maude functional programs the key formal property checked is the Church-Rosser property. For concurrent declarative programs in rewriting logic, the key property checked is the coherence between rules and equations modulo the axioms A. Such properties are essential, both for executability purposes and as a basis for verifying many other properties, such as, for example, proving inductive theorems of a functional program, or correct model checking of temporal logic properties for a concurrent program. This paper develops the mathematical foundations on which the checking of these properties (or ground versions of them) is based, presents two tools, the Church-Rosser Checker (CRC) and the Coherence Checker (ChC) supporting the verification of these properties, and illustrates with examples a methodology to establish such properties using the proof obligations returned by the tools.
KW - Church-Rosser property
KW - Coherence
KW - Formal verification
KW - Maude
KW - Order-sorted conditional specifications
KW - Rewriting modulo
UR - http://www.scopus.com/inward/record.url?scp=84868142933&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84868142933&partnerID=8YFLogxK
U2 - 10.1016/j.jlap.2011.12.004
DO - 10.1016/j.jlap.2011.12.004
M3 - Article
AN - SCOPUS:84868142933
VL - 81
SP - 816
EP - 850
JO - Journal of Logic Programming
JF - Journal of Logic Programming
SN - 1567-8326
IS - 7-8
ER -