摘要翻译：
本文是我们对计算机代数语言MiniMaple（Maple的一个重要子集，略有扩展）所写程序的形式化说明的初步结果的一个基于实例的演示。这项工作的主要目标是为Minimaple定义一个验证框架。最小程序的形式化说明是一项复杂的工作，因为它支持非标准类型的对象，如符号和未求值的表达式，以及附加的函数和谓词，如运行时类型测试等。我们用形式化说明语言来说明我所开发的Maple包差分程序中的各种计算机代数概念和相应的对象。
---
英文标题：
《On Formal Specification of Maple Programs》
---
作者：
Muhammad Taimoor Khan, Wolfgang Schreiner
---
最新提交年份：
2012
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Mathematical Software        数学软件
分类描述：Roughly includes material in ACM Subject Class G.4.
大致包括ACM学科类G.4的材料。
--
一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  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.
---
PDF链接：
https://arxiv.org/pdf/1207.2291