Frontiers of Information Technology (2012)
Islamabad, Pakistan Pakistan
Dec. 17, 2012 to Dec. 19, 2012
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/FIT.2012.38
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.
specification language, formal semantics, Maple
M. T. Khan, "On the Formal Semantics of MiniMaple and its Specification Language," 2012 10th International Conference on Frontiers of Information Technology (FIT 2012)(FIT), Islamabad, 2012, pp. 169-174.