The Community for Technology Leaders
Frontiers of Information Technology (2012)
Islamabad, Pakistan Pakistan
Dec. 17, 2012 to Dec. 19, 2012
ISBN: 978-1-4673-4946-8
pp: 169-174
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
99 ms
(Ver 3.3 (11022016))