| An Arithmetical Module for Rationals and Reals (1997) | |||||||||||||||
Abstract | |||||||||||||||
| This paper is a sequel to our earlier paper [BS96]. We continue our project to develop a family of data type specifications starting from elementary principles and in a setting of four-valued logic. We refer to [BBR95] for a discussion on this particular four-valued logic, and to [BS96] for a discussion on its use. The objective of this document is to provide a number of data types between naturals and rationals: natural numbers, fractions in various notations and fixed- and floating point reals in arbitrary precision. These fixed point reals result from rounding off which occurs if a decimal notation for a fraction is needed. The specifications have been produced, typechecked and simulated using the ASF+SDF system [Kli95]. This system combines algebraic specifications [BHK85] with the Syntax Definition Formalism SDF [HK89]. We specify abstract syntax only. No module for pretty printing is provided. We notice that for full use in ASF+SDF the pretty printing options of ASF+SDF are not yet satisfactory. Equations like | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||