IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

On the Church-Rosser and Coherence Properties of Conditional Order-Sorted Rewrite Theories

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/17384

Files in this item

File Description Format
PDF CRChC.pdf (478KB) (no description provided) PDF
Title: On the Church-Rosser and Coherence Properties of Conditional Order-Sorted Rewrite Theories
Author(s): Duran, Francisco; Meseguer, José
Subject(s): Maude order-sorted conditional specifications rewriting modulo formal verification Church-Rosser property coherence
Abstract: 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 quite expressive 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; and (b) order-sorted conditional rewrite theories R = (Σ, E ∪ A, R, φ), corresponding to concurrent programs modulo axioms A. For 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 Maude 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.
Issue Date: 2010-11-03
Genre: Technical Report
Type: Text
Language: English
URI: http://hdl.handle.net/2142/17384
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2010-11-03
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 169
  • Downloads this Month: 0
  • Downloads Today: 0

Browse

My Account

Information

Access Key