Simultaneous Checking of Completeness and Ground Confluence

c specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a correct and modular way. Related works for checking ground confluence are based on the completion techniques or on the test that all critical pairs between axioms are valid w.r.t. a sufficient criterion for ground confluence. It is generally accepted that such techniques may be very inefficient even for very small specifications. Indeed, the completion procedure often diverges and there often exist many critical pairs of the axioms. In this paper, we present a procedure for simultaneously checking completeness and ground confluence for specifications with free/non-free constructors and parameterized specifications. If the specification is not complete or not ground confluent, then our procedure will output the set of patterns on whose ground instances a...

• Type: Conference
• Year: 2000
• Where: KBSE
• Authors: Adel Bouhoula
• Keywords: Critical Pairs, Ground Confluence, KBSE 2000, Software Engineering, Specifications