Submitted Paper
| ID | 28 |
| Submitted | 2006-04-21 |
| Last Update | |
| Title | Sufficient Completeness Checking with Propositional Tree Automata |
| Author(s) | Author #1 Name: Joe Hendrix Org: University of Illinois, Urbana-Champaign Country: USA Email: jhendrix@uiuc.edu Author #2 Name: Jose Meseguer Org: University of Illinois, Urbana-Champaign Country: USA Email: jhendrix@uiuc.edu Author #3 Name: Hitoshi Ohsaki Org: National Instiution of Advanced Industrial Science and Technology Country: Japan Email: ohsaki@ni.aist.go.jp |
| Other Author(s) | |
| Contact Author | Author #1 Alt Email: Telephone: (217) 417-5221 |
| Keywords | Sufficient completeness, equational logic, tree automata |
| Abstract | A specification is sufficiently complete when its functions are fully defined on all relevant data. This is important for both debugging and formal reasoning. Although sufficient completeness is well-studied on unsorted and unconditional specifications, it has not been extensively studied in the more expressive logics supported by advanced equational specification and programming languages. In this work [3], we extend sufficient completeness methods to handle more expresssive specifications involving: (i) partiality; (ii) conditional equations; and (iii) deduction modulo axioms. Specifically, we give useful characterizations of the sufficient completeness property for membership equational logic (MEL) specifications having features (i)--(iii). This characterization of sufficient completeness allows us to extend the soundness of the method in [2] to a larger class of specifications. Furthermore, this characterization opens the door to new tree automata-based methods for checking order-sorted specifications with rewriting modulo equations. Using recent results on propositional tree automata [1], a class of tree automata closed under Boolean operations and an equational theory, we are able to check the sufficient completeness of many order-sorted and linear specifications with rewriting modulo any combination of associativity, commutativity, and identity. The methods presented here can serve as a basis for building a next-generation sufficient completeness tool for MEL specifications having features (i)--(iii). These features are widely used in practice, and are supported by languages such as Maude and other advanced specification and equational programming languages.
|
| Topics | |
| Comments | |
| Paper | 28.pdf (59KB) |