Equational specifications: design, implementation, and reasoning

  • S. Antoy
  • P. Forcheri
  • J. Gannon
  • M. T. Molfino
Part of the Texts and Monographs in Symbolic Computation book series (TEXTSMONOGR)


Sets of equations specify software systems either by describing the result of a computation or by characterizing some properties of the result. Suppose that the problem at hand is that of sorting a sequence of elements.


Inductive Hypothesis Theorem Prover Direct Implementation Inductive Variable Abstract Data Type 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Antoy, S. (1990): Design strategies for rewrite rules. In: Kaplan, S., Okada, M. (eds.): Conditional and typed rewriting systems. Springer, Berlin Heidelberg New York Tokyo, pp. 333–341 (Lecture notes in computer science, vol. 516).Google Scholar
  2. Antoy, S., Gannon, J. (1994): Using term rewriting system to verify software. IEEE Trans. Software Eng. 20: 259–274.CrossRefGoogle Scholar
  3. Antoy, S., Hamlet, D. (1992): Automatically checking an implementation against its formal specifications. In: Shelby, E. R. W. (ed.): Proceedings 2nd Irvine Software Symposium, Irvine, CA, pp. 29–48.Google Scholar
  4. Antoy, S., Forcheri, P., Molfino, M. T. (1990): Specification-based code generation. In: Shriver, B. D. (ed.): Proceedings 23rd Hawaii International Conference on System Sciences, vol. II, software. IEEE Computer Society Press, Los Alamitos, pp. 165–173.Google Scholar
  5. Antoy, S., Forcheri, P., Molfino, M., Schenone, C. (1993): A uniform approach to deduction and automatic implementation. In: Fitch, J. (ed.): Design and implementation of symbolic computation systems. Springer, Berlin Heidelberg New York Tokyo, pp. 132–144 (Lecture notes in computer science, vol. 721).CrossRefGoogle Scholar
  6. Avizienis, A., Kelly, J. (1984): Fault tolerance by design diversity: concepts and experiments. Computer 17: 67–80.CrossRefGoogle Scholar
  7. Basu, S. (1980): On development of iterative programs from functional specifications. IEEE Trans. Software Eng. 6: 170–182.zbMATHCrossRefGoogle Scholar
  8. Boyer, R., Moore, J. (1979): A computational logic. Academic Press, Orlando.zbMATHGoogle Scholar
  9. Burstall, R. (1969): Proving properties of programs by structural induction. Comput. J. 12: 41–48.zbMATHGoogle Scholar
  10. Choppy, C., Kaplan, S., Soria, M. (1989): Complexity analysis of term-rewriting systems. Theor. Comput. Sci. 67: 261–282.MathSciNetzbMATHCrossRefGoogle Scholar
  11. Clocksin, W., Mellish, C. (1984): Programming in Prolog, 2nd edn. Springer, Berlin Heidelberg New York Tokyo.CrossRefGoogle Scholar
  12. Dershowitz, N., Jouannaud, J. (1990): Rewrite systems. In: van Leeuwen, J. (ed.): Handbook of theoretical computer science B: formal methods and semantics. North-Holland, Amsterdam, pp. 243–320.Google Scholar
  13. Ehrig, H., Mahr, B. (1985): Fundamentals of algebraic specifications 1: equations and initial semantics. Springer, Berlin Heidelberg New York Tokyo.CrossRefGoogle Scholar
  14. Garland, S. J., Guttag, J. V., Horning, J. J. (1990): Debugging Larch shared language specifications. IEEE Trans. Software Eng. 16: 1044–1057.CrossRefGoogle Scholar
  15. Goguen, J. A. (1978): Order sorted algebras. Tech. Rep. 14, Computer Science Department, University of California Los Angeles.Google Scholar
  16. Goguen, J. A., Winkler, T. (1988): Introducing OBJ3. Tech. Rep. SRI-CSL-88-9, SRI International, Menlo Park, CA.Google Scholar
  17. Guttag, J. V., Horowitz, E., Musser, D. (1978): Abstract data types and software validation. Commun. ACM 21: 1048–1064.MathSciNetzbMATHCrossRefGoogle Scholar
  18. Hoare, C. A. R. (1972): Proof of correctness of data representations. Acta Inf. 1: 271–281.zbMATHCrossRefGoogle Scholar
  19. Klop, J. (1992): Term rewriting systems. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.): Handbook of logic in computer science. Oxford University Press, Oxford, pp. 1–112.Google Scholar
  20. Knight, J. C., Leveson, N. G. (1986): An experimental evaluation of the assumption of independence in multi-version programming. IEEE Trans. Software Eng. 12: 96–109.CrossRefGoogle Scholar
  21. Knuth, D. E., Bendix, P. B. (1970): Simple word problems in universal algebras. In: Leech, J. (ed.): Computational problems in abstract algebra. Pergamon, Oxford, pp. 263–297.Google Scholar
  22. Leveson, N. G., Cha, S. S., Knight, J. C., Shimeall, T. J. (1990): The use of self checks and voting in software detection: an empirical study. IEEE Trans. Software Eng. 16: 432–443.CrossRefGoogle Scholar
  23. Luckham, D. C. (1990): Programming with specifications: an introduction to ANNA, a language for specifying Ada programs. Springer, Berlin Heidelberg New York Tokyo.zbMATHGoogle Scholar
  24. Meyer, B. (1988): Object-oriented software construction. Prentice-Hall, Englewood Cliffs.Google Scholar
  25. van Emden, M. H., Yukawa, K. (1987): Logic programming with equations. Logic Program. 4: 265–288.zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Wien 1997

Authors and Affiliations

  • S. Antoy
  • P. Forcheri
  • J. Gannon
  • M. T. Molfino

There are no affiliations available

Personalised recommendations