On formal specification of Maple programs

DOI10.1007/978-3-642-31374-5_33zbMATH Open1360.68939arXiv1207.2291OpenAlexW2151263772MaRDI QIDQ2907346FDOQ2907346

Authors: Muhammad Taimoor Khan, Wolfgang Schreiner 

Publication date: 7 September 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1207.2291

Recommendations

• Towards the formal specification and verification of Maple programs
• scientific article; zbMATH DE number 1262431
• scientific article; zbMATH DE number 2009891
• scientific article; zbMATH DE number 53947
• scientific article; zbMATH DE number 3936493

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (2)

• Towards the formal specification and verification of Maple programs
• Compiling dyadic first-order specifications into map algebra

Uses Software

• Maple
• Why3
• MiniMaple
• DifferenceDifferential

This page was built for publication: On formal specification of Maple programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907346)