Lightweight formal methods for computer algebra systems

Abstract

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.