On Formal Specification of Maple Programs

TL;DR

This paper demonstrates initial results on formally specifying MiniMaple programs, a subset of Maple, to enable verification, addressing complexities like non-standard types and specialized functions.

Contribution

It introduces a formal specification framework for MiniMaple, facilitating program verification in the context of computer algebra systems.

Findings

Specification of complex data types like symbols and unevaluated expressions

Formalization of computer algebra concepts within MiniMaple

Development of a verification framework for MiniMaple programs

Abstract

This paper is an example-based demonstration of our initial results on the formal specification of programs written in the computer algebra language MiniMaple (a substantial subset of Maple with slight extensions). The main goal of this work is to define a verification framework for MiniMaple. Formal specification of MiniMaple programs is rather complex task as it supports non-standard types of objects, e.g. symbols and unevaluated expressions, and additional functions and predicates, e.g. runtime type tests etc. We have used the specification language to specify various computer algebra concepts respective objects of the Maple package DifferenceDifferential developed at our institute.