Towards the Formal Specification and Verification of Maple Programs

TL;DR

This paper discusses the initial development of formal methods for specifying and verifying MiniMaple programs, aiming to detect behavioral errors through static analysis in a complex computer algebra language.

Contribution

It introduces a formal syntax, semantics, type system, and specification language for MiniMaple, addressing the unique challenges of computer algebra languages.

Findings

Defined formal syntax and semantics for MiniMaple

Developed a type system for MiniMaple

Established a specification language for MiniMaple

Abstract

In this paper, we present our ongoing work and initial results on the formal specification and verification of MiniMaple (a substantial subset of Maple with slight extensions) programs. The main goal of our work is to find behavioral errors in such programs w.r.t. their specifications by static analysis. This task is more complex for widely used computer algebra languages like Maple as these are fundamentally different from classical languages: they support non-standard types of objects such as symbols, unevaluated expressions and polynomials and require abstract computer algebraic concepts and objects such as rings and orderings etc. As a starting point we have defined and formalized a syntax, semantics, type system and specification language for MiniMaple.