Frontiers of Information Technology (2012)

Islamabad, Pakistan Pakistan

Dec. 17, 2012 to Dec. 19, 2012

ISBN: 978-1-4673-4946-8

pp: 169-174

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/FIT.2012.38

ABSTRACT

In this paper, we give a definition of the formal (denotational) semantics of MiniMaple (a substantial subset of a widely used computer algebra system Maple with slight modifications) and its specification language. Defining the formal semantics of MiniMaple and its specification language is rather a challenging task as these support non-standard types of objects, e.g. symbols, unions and polynomials, and additional predicates and functions, e.g. runtime type tests etc. Furthermore, the specification language also supports logical and sequence quantifiers and numeric quantifiers with a logical condition (property) to quantify a filtered range of values. This semantics is defined as a pre-requisite of a verification calculus which we are currently developing. The verification conditions generated by the verification calculus must be sound w.r.t. defined formal semantics.

INDEX TERMS

specification language, formal semantics, Maple

CITATION

Muhammad Taimoor Khan,
"On the Formal Semantics of MiniMaple and its Specification Language",

*Frontiers of Information Technology*, vol. 00, no. , pp. 169-174, 2012, doi:10.1109/FIT.2012.38