Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications

  • Masaki Nakamura
  • Kazuhiro Ogata
  • Kokichi Futatsugi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


OBJ languages support semi-automated verification for algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination, confluence and sufficient completeness are important fundamental properties for the equational reasoning. In this article, we give light-weight methods for checking those properties in a modular way. We formalize the notion of hierarchical extension for constructor-based conditional algebraic specifications, and give sufficient conditions for those fundamental properties, which can be used for proving them incrementally.


conditional term rewriting systems algebraic specifications termination confluence sufficient completeness incremental proofs 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Bouhoula, A., Jacquemard, F.: Sufficient Completeness Verification for Conditional and Constrained Term Rewriting Systems. Journal of Applied Logic 10(1), 127–143 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Futatsugi, K., Găină, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theor. Comput. Sci. 464, 90–112 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Software Engineering with OBJ: Algebraic Specification in Action. In: Introducing OBJ*. Kluwers Academic Publishers (2000)Google Scholar
  5. 5.
    Guttag, J.V.: The specification and application to programming of abstract data types. PhD thesis, University of Toronto, Toronto, Ont., Canada, Canada (1975)Google Scholar
  6. 6.
    Hsiang, J.: Refutational theorem proving using term-rewriting systems. Artif. Intell. 25(3), 255–300 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Jouannaud, J.-P., Kirchner, C., Kirchner, H., Mégrelis, A.: OBJ: Programming with equalities, subsorts, overloading and parameterization. In: Grabowski, J., Lescanne, P., Wechler, W. (eds.) ALP 1988. LNCS, vol. 343, pp. 41–52. Springer (1988)Google Scholar
  8. 8.
    Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Inf. 28(4), 311–350 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Kong, W., Ogata, K., Futatsugi, K.: Towards reliable e-government systems with the OTS/CafeOBJ method. IEICE Transactions 93-D(5), 974–984 (2010)CrossRefGoogle Scholar
  10. 10.
    Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95(4), 446–453 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Marché, C., Urbain, X.: Modular and incremental proofs of ac-termination. J. Symb. Comput. 38(1), 873–897 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Nakamura, M., Ogata, K., Futatsugi, K.: Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications. J. Symb. Comput. 45(5), 551–573 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Nakamura, M., Ogata, K., Futatsugi, K.: On proving operational termination incrementally with modular conditional dependency pairs. IAENG International Journal of Computer Science 40(2), 117–123 (2013)Google Scholar
  14. 14.
    Nakamura, M., Ogawa, K., Futatsugi, K.: A hierarchical approach to operational termination of algebraic specifications. In: Proceedings of the International Conference on Electronics, Information and Communication, ICEIC 2013, pp. 144–145 (2013)Google Scholar
  15. 15.
    Ogata, K., Futatsugi, K.: Proof scores in the OTS/CafeOBJ Method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  16. 16.
    Ohlebusch, E.: Advanced Topics in Term Rewriting, 1st edn. Springer Publishing Company, Incorporated (2010)zbMATHGoogle Scholar
  17. 17.
    Ouranos, I., Ogata, K., Stefaneas, P.: Formal analysis of tesla protocol in the timed OTS/CafeOBJ method. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 126–142. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  18. 18.
    Schernhammer, F., Meseguer, J.: Incremental checking of well-founded recursive specifications modulo axioms. In: Schneider-Kamp, P., Hanus, M. (eds.) PPDP, pp. 5–16. ACM (2011)Google Scholar
  19. 19.
    Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)Google Scholar
  20. 20.
    Urbain, X.: Modular & incremental automated termination proofs. J. Autom. Reasoning 32(4), 315–355 (2004)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Masaki Nakamura
    • 1
  • Kazuhiro Ogata
    • 2
  • Kokichi Futatsugi
    • 2
  1. 1.Toyama Prefectural UniversityImizuJapan
  2. 2.Japan Advanced Institute of Science and TechnologyNomiJapan

Personalised recommendations