Abstract
We demonstrate the use of formal methods tools to provide a semantics for the type hierarchy of the AXIOMcomputer algebra system, and a methodology for Aldor program analysis and verification. We give a case study of abstract specifications of AXIOM primitives, and provide an interface between these abstractions and Aldor code.
Funded by NAG Ltd
Acknowledgements
We acknowledge support of the UK EPSRC under grant number GR/L48256 and of NAG Ltd. We also thank James Davenport of the University of Bath and Mike Dewar from NAG for their interest and suggestions.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Ballarin, C., Homann, K., AND Calmet, J. Theorems and algorithms: An interface between Isabelle and Maple. In Proceedings of International Symposium on Symbolic and Algebraic Computation (1995), A.H.M. Levelt, Ed., ACM Press, pp. 150–157.
Bauer, A., Clarke, E., AND Zhao, X. Analytica—an experiment in combining theorem proving and symbolic computation. J. Automat. Reason. 21, 3 (1998), 295–325.
Buchberger, B. Symbolic computation: computer algebra and logic. In Frontiers of combining systems (Munich, 1996). Kluwer Acad. Publ., Dordrecht, 1996, pp. 193–219.
Char, B. W. Maple V language Reference Manual. Springer-Verlag, 1991.
Cheon, Y., AND Leavens, G. T. A gentle introduction to Larch/Smalltalk specification browsers. Tech. Rep. TR 94-01, Department of Computer Science, Iowa State University, 226 Atanaso Hall, Ames, Iowa 50011-1040, USA, Jan. 1994.
Detlefs, D. L. An overview of the Extended Static Checking system. In Proceedings of The First Workshop on Formal Methods in Software Practice (Jan 1996), ACM (SIGSOFT), pp. 1–9.
Dingle, A., AND Fateman, R. J. Branch cuts in computer algebra. In Symbolic and Algebraic Computation (1994), ISSAC, ACM Press.
Dolzmann, A., AND Sturm, T. REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31, 2 (June 1997), 2–9.
Dunstan, M., Kelsey, T., Linton, S., AND Martin, U. Lightweight formal methods for computer algebra systems. In ISSAC (1998).
Evans, D. Using specifications to check source code. Master’s thesis, Department of Electrical Engineering and Computer Science, MIT Lab. for Computer Science, 545 Technology Square, Cambridge, MA 02139, June 1994.
Feit, W., AND Thompson, J. G. Solvability of groups of odd order. Pacific Journal of Mathematics 13 (1963), 775–1029.
The GAP Group. GAP Groups, Algorithms, and Programming, Version 4. Aachen, St Andrews, 1998. (http://www-gap.dcs.st-and.ac.uk/~gap).
Gordon, M. J. C. Programming language theory and its implementation. Series in Computer Science. Prentice Hall International, 1988.
Gordon, M. J. C., AND Melham, T. F., Eds. Introduction to HOL. Cambridge University Press, Cambridge, 1993. A theorem proving environment for higher order logic, Appendix B by R. J. Boulton.
Guaspari, D., Marceau, C., AND Polak, W. Formal verification of Ada programs. In First International Workshop on Larch (July 1992), U. Martin and J. Wing, Eds., Springer-Verlag, pp. 104–141.
Guttag, J. V., AND Horning, J. J. Larch: Languages and Tools for Formal Specification, first ed. Texts and Monograps in Computer Science. Springer-Verlag, 1993.
Harrison, J., AND Théry, L. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In Higher order logic theorem proving and its applications (Vancouver, BC, 1993). Springer, Berlin, 1994, pp. 174–184.
Jackson, P. Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Apr. 1995.
Jenks, R. D., AND Sutor, R. S. AXIOM. Numerical Algorithms Group Ltd., Oxford, 1992. The scientific computation system, With a foreword by David V. Chudnovsky and Gregory V. Chudnovsky.
Jones, C. B. Systematic Software Development using VDM, second ed. Computer Science. Prentice Hall International, 1990.
Jones, K. D. LM3: a Larch interface language for Modula-3, a definition and introduction. Tech. Rep. 72, SRC, Digital Equipment Corporation, Palo Alto, California, June 1991.
King, D. J., AND Arthan, R. D. Development of practical verification tools. The ICL Systems Journal 1 (May 1996).
Leavens, G. T., AND Cheon, Y. Preliminary design of Larch/C+ +. In First International Workshop on Larch (July 1992), U. Martin and J. M. Wing, Eds., Workshops in Computing, Springer-Verlag, pp. 159–184.
Meyer, B. Object-Oriented Software Construction. Computer Science. Prentice Hall International, 1988.
Owre, S., Shankar, N., AND Rushby, J. M. User Guide for the PVS Specification and Verification System. Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1993.
Poll, E., AND Thompson, S. Adding the axioms to Axiom: Towards a system of automated reasoning in aldor. Technical Report 6-98, Computing Laboratory, University of Kent, May 1998.
Potter, B., Sinclair, J., AND Till, D. An introduction to formal specification and Z. Prentice Hall International, 1991.
Sannella, D. Formal program development in Extended ML for the working programmer. In Proceedings of the 3rd BCS/FACS Workshop on Refinement (1990), Springer Workshops in Computing, pp. 99–130.
Vandevoorde, M. T., AND Guttag, J. V. Using specialized procedures and specification-based analysis to reduce the runtime costs of modularity. In Proceedings of the 1994 ACM/SIGSOFT Foundations of Software Engineering Conference (1994).
Wing, J. M. A two-tiered approach to specifying programs. Tech. Rep. LCS/TR-299, Laboratory for Computer Science, MIT, May 1983.
Wing, J. M., Rollins, E., AND Zaremski, A. M. Thoughts on a Larch/ML and a new application for TP. In First International Workshop on Larch (July 1992), U. Martin and J. M. Wing, Eds., Workshops in Computing, Springer-Verlag, pp. 297–312.
Wolfram, S. Mathematica: A system for doing mathematics by computer, 2 ed. Addison Wesley, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dunstan, M.N., Kelsey, T., Martin, U., Linton, S. (1999). Formal methods for extensions to CAS. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_43
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive