An Algorithm to Test for Confluence in a System of Left to Right Rewrite Rules.

Abstract

Formal specifications of computation systems promise to afford us not only a strictly enforced discipline in describing the semantics of the system, but also a way of proving that the system functions as described. There exists a rich body of mathematical theory regarding the use of formal specifications. However, the bridge from the theoretical world to the practical world is nonexistent in most cases. This research concentrates on developing practical techniques to determine the correctness of a formal specification. The foundation for the specifications we describe is in abstract algebras. However, the view of the axioms for a specification is modified so that axioms are treated as left to right rewrite rules, rather than as mathematical equalities. The major result of the research is a new and practical algorithm to determine confluence in an axiom system of left to right rewrite rules that satisfy certain restrictions.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1984
Accession Number
ADA154066

Entities

People

  • R. Griffin

Organizations

  • Naval Postgraduate School

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • California
  • Classification
  • Computations
  • Computer Science
  • Computers
  • Confluence
  • Environment
  • Mathematics
  • Security
  • Semantics
  • Sequences
  • Specifications
  • Standards
  • Template Patterns
  • United States

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Software Engineering.
  • Systems Analysis and Design