A Church-Rosser Checker Tool for Maude Equational Specifications

Francisco Durán and José Meseguer

This document explains the design and use of a Church-Rosser checker tool, which checks whether an equational specification satisfies the Church-Rosser property. This tool can be used to prove the Church-Rosser property of order-sorted equational specifications in Maude. The tool has been written entirely in Maude and is in fact an executable specification in rewriting logic of the formal inference system that it implements. The fact that rewriting logic is reflective, and that Maude efficiently supports reflective rewriting logic computations is systematically exploited in the design of the tool.

(BibTeX entry)    (gzip'ed Postscript)   

back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International