Lightweight formal methods for computer algebra systems
Martin Dunstan, Tom Kelsey, Steve Linton, Ursula Martin · 1998
In this paper we demonstrate the use of formal methods tools to provide a semantics for the type hierarchy of the AXIOM computer algebra system, and a methodology for Aldor program analysis and verification. We give examples of abstract specifications of AXIOM primitives, and provide an interface between these abstractions and Aldor code. 1 Introduction We describe work in progress at St Andrews to apply formal methods and machine assisted theorem proving techniques to improve the robustness and reliability of computer algebra systems. This project considers the use of the Larch [7] approach to formal methods through specifications and uses AXIOM [8] for the computer algebra system. We do not exclude other formal methods systems such as VDM [9] or Z [13] nor do we exclude applications to other computer algebra systems (CAS) such as Mathematica [17] or Maple [14]. Indeed the weaker type systems used by the latter packages may benefit more from our approach than AXIOM can. In the remai...