Abstract
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.
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
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).
Antoy, S., Gannon, J. (1994): Using term rewriting system to verify software. IEEE Trans. Software Eng. 20: 259–274.
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.
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.
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).
Avizienis, A., Kelly, J. (1984): Fault tolerance by design diversity: concepts and experiments. Computer 17: 67–80.
Basu, S. (1980): On development of iterative programs from functional specifications. IEEE Trans. Software Eng. 6: 170–182.
Boyer, R., Moore, J. (1979): A computational logic. Academic Press, Orlando.
Burstall, R. (1969): Proving properties of programs by structural induction. Comput. J. 12: 41–48.
Choppy, C., Kaplan, S., Soria, M. (1989): Complexity analysis of term-rewriting systems. Theor. Comput. Sci. 67: 261–282.
Clocksin, W., Mellish, C. (1984): Programming in Prolog, 2nd edn. Springer, Berlin Heidelberg New York Tokyo.
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.
Ehrig, H., Mahr, B. (1985): Fundamentals of algebraic specifications 1: equations and initial semantics. Springer, Berlin Heidelberg New York Tokyo.
Garland, S. J., Guttag, J. V., Horning, J. J. (1990): Debugging Larch shared language specifications. IEEE Trans. Software Eng. 16: 1044–1057.
Goguen, J. A. (1978): Order sorted algebras. Tech. Rep. 14, Computer Science Department, University of California Los Angeles.
Goguen, J. A., Winkler, T. (1988): Introducing OBJ3. Tech. Rep. SRI-CSL-88-9, SRI International, Menlo Park, CA.
Guttag, J. V., Horowitz, E., Musser, D. (1978): Abstract data types and software validation. Commun. ACM 21: 1048–1064.
Hoare, C. A. R. (1972): Proof of correctness of data representations. Acta Inf. 1: 271–281.
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.
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.
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.
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.
Luckham, D. C. (1990): Programming with specifications: an introduction to ANNA, a language for specifying Ada programs. Springer, Berlin Heidelberg New York Tokyo.
Meyer, B. (1988): Object-oriented software construction. Prentice-Hall, Englewood Cliffs.
van Emden, M. H., Yukawa, K. (1987): Logic programming with equations. Logic Program. 4: 265–288.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer-Verlag Wien
About this chapter
Cite this chapter
Antoy, S., Forcheri, P., Gannon, J., Molfino, M.T. (1997). Equational specifications: design, implementation, and reasoning. In: Miola, A., Temperini, M. (eds) Advances in the Design of Symbolic Computation Systems. Texts and Monographs in Symbolic Computation. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6531-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6531-7_8
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-82844-1
Online ISBN: 978-3-7091-6531-7
eBook Packages: Springer Book Archive