Advertisement

Combining algebraic and set-theoretic specifications

  • Claus Hintermeier
  • Hélène Kirchner
  • Peter D. Mosses
Contributions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)

Abstract

Specification frameworks such as B and Z provide power sets and cartesian products as built-in type constructors, and employ a rich notation for defining (among other things) abstract data types using formulae of predicate logic and lambda-notation. In contrast, the so-called algebraic specification frameworks often limit the type structure to sort constants and first-order functionalities, and restrict formulae to (conditional) equations. Here, we propose an intermediate framework where algebraic specifications are enriched with a set-theoretic type structure, but formulae remain in the logic of equational Horn clauses. This combines an expressive yet modest specification notation with simple semantics and tractable proof theory.

Keywords

Inference Rule Choice Function Unify Algebra Variable Assignment Horn Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J. R. Abrial. B-Tool Reference Manual. Edinburgh Portable Compiler, 1991.Google Scholar
  2. 2.
    L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N. Y., USA), volume 607 of Lecture Notes in Computer Science, pages 462–476. Springer-Verlag, 1992.Google Scholar
  3. 3.
    J. Dawes. The VDM-SL Reference Guide. Pitman, 1991.Google Scholar
  4. 4.
    N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 & 2):69–116, 1987.Google Scholar
  5. 5.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Equations and initial semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.Google Scholar
  6. 6.
    C. Hintermeier. Déduction avec sortes ordonnées et égalités. Thèse de Doctorat d'Université, Université Henri Poincaré-Nancy 1, Oct. 1995.Google Scholar
  7. 7.
    C. Hintermeier, H. Kirchner, and P. D. Mosses. Combining algebraic and settheoretic specifications (extended version). Technical report, Centre de Recherche en Informatique de Nancy, 1996.Google Scholar
  8. 8.
    C. Hintermeier, H. Kirchner, and P. D. Mosses. R n- and G n-logics. In Proceedings of Second International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Paderborn (Germany), Sept. 1995.Google Scholar
  9. 9.
    T. S. E. Maibaum and C. J. Lucena. Higher order data types. International Journal of Computer and Information Sciences, 9:31–53, 1980.Google Scholar
  10. 10.
    V. Manca, A. Salibra, and G. Scollo. Equational type logic. Theoretical Computer Science, 77(1–2): 131–159, 1990.Google Scholar
  11. 11.
    K. Meinke. Universal algebra in higher types. Theoretical Computer Science, 100:385–417, 1992.Google Scholar
  12. 12.
    B. Möller. Algebraic specifications with high-order operators. In L. Meertens, editor, Proceedings IFIP TC2 Working Conf. on Program Specification and Transformation, pages 367–392. IFIP, Elsevier Science Publishers B. V. (North-Holland), 1987.Google Scholar
  13. 13.
    B. Möller, A. Tarlecki, and M. Wirsing. Algebraic specification with built-in domain constructions. In M. Dauchet and M. Nivat, editors, Proceedings of CAAP'88, Lecture Notes in Computer Science, pages 132–148. Springer-Verlag, 1988.Google Scholar
  14. 14.
    B. Möller, A. Tarlecki, and M. Wirsing. Algebraic specifications or reachable higher-order algebras. In D. Sannella and A. Tarlecki, editors, Recent Trends in Data Type Specification, volume 332 of Lecture Notes in Computer Science, pages 154–169. Springer-Verlag, 1988.Google Scholar
  15. 15.
    P. D. Mosses. Unified algebras and institutions. In Proceedings 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, pages 304–312, 1989.Google Scholar
  16. 16.
    R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N. Y., USA), volume 607 of Lecture Notes in Computer Science, pages 477–491. Springer-Verlag, 1992.Google Scholar
  17. 17.
    A. Poigné. Partial algebras, subsorting and dependent types. prerequisites of error handling in algebraic specifications. In Proceedings of Workshop on Abstract Data Types, volume 332 of Lecture Notes in Computer Science. Springer-Verlag, 1988.Google Scholar
  18. 18.
    J. M. Spivey. Understanding Z: a specification language and its formal semantics. Cambridge University Press, 1988.Google Scholar
  19. 19.
    A. N. Whitehead and B. Russell. Principia Mathematica, volume 1. Cambridge University Press, Cambridge, MA, 1925.Google Scholar
  20. 20.
    M. Wirsing. Algebraic specification. In J. van Leeuwen, A. Meyer, M. Nivat, M. Paterson, and D. Perrin, editors, Handbook of Theoretical Computer Science, volume B, chapter 13. Elsevier Science Publishers B. V. (North-Holland) and The MIT press, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Claus Hintermeier
  • Hélène Kirchner
    • 1
  • Peter D. Mosses
    • 2
  1. 1.CRIN-CNRS & INRIA-LorraineVandœuvre-lès-Nancy CedexFrance
  2. 2.BRICS, Dept. of Computer ScienceUniversity of AarhusAarhus CDenmark

Personalised recommendations