Abstract
We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude’s inductive theorem prover (ITP) that is used as a backend to try to automatically discharge those proof obligations.
Research supported by Grants ONR N00014-02-1-0715, NSF CCR-0234524, and Spanish MCYT Projects TIC2002-01167 and TIC2003-01000.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)
Meseguer, J., Roşu, G.: A total approach to partial algebraic specification. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 572–584. Springer, Heidelberg (2002)
Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 2–16. Springer, Heidelberg (2003)
Kapur, D., Subramaniam, M.: New uses of linear arithmetic in automated theorem proving by induction. Journal of Automated Reasoning 16, 39–78 (1996)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Mart´ı-Oliet, N., Meseguer, J., Quesada, J.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Misra, J.: Powerlist: a structure for parallel recursion. ACM Transactions on Programming Languages and Systems 16, 1737–1767 (1994)
Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications (extended technical report) (2005), Available on tool website at http://maude.cs.uiuc.edu/tools/scc/
Clavel, M.: The ITP tool’s home page (2005), http://maude.sip.ucm.es/itp
Guttag, J.: The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto Computer Science Department, Report CSRG-59 (1975)
Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Inf. 10, 27–52 (1978)
Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) GI-TCS 1983. LNCS, vol. 145, pp. 257–268. Springer, Heidelberg (1982)
Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24, 395–415 (1987)
Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28, 311–350 (1991)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), Available on: http://www.grappa.univ-lille3.fr/tata release (October 1, 2002)
Bouhoula, A., Rusinowitch, M.: SPIKE: A system for automatic inductive proofs. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 576–577. Springer, Heidelberg (1995)
Kapur, D.: An automated tool for analyzing completeness of equational specifications. In: Proceedings of the 1994 International Symposium on Software Testing and Analysis (ISSTA), Seattle, WA, USA. Software Engineering Notes, Special Issue, August 17-19, pp. 28–43. ACM Press, New York (1994)
Ohsaki, H., Seki, H., Takai, T.: Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 483–498. Springer, Heidelberg (2003)
Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: Cafe: An Industrial-Strength Algebraic Formal Method, Elsevier, Amsterdam (2000)
Durán, F., Lucas, S., Meseguer, J., Marché, C., Urbain, X.: Proving termination of membership equational programs. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, Verona, Italy, August 24-25, pp. 147–158. ACM Press, New York (2004)
Lucas, S., Meseguer, J., Marché, C.: Operational termination of generalized conditional term rewriting systems. Submitted (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hendrix, J., Clavel, M., Meseguer, J. (2005). A Sufficient Completeness Reasoning Tool for Partial Specifications. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-32033-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25596-3
Online ISBN: 978-3-540-32033-3
eBook Packages: Computer ScienceComputer Science (R0)