|
| |||||
| 9.1 Introduction | ||||||
The SML translator was written by Ke Wei, as reported in [4].
We use the term RSLSML for the subset of RSL that is accepted by the the translator. RSLSML excludes object arrays, channels, axioms, abstract types, union types, implicit value and function definitions. It only includes quantified expressions, comprehended expressions, and implicit let expressions if they conform to the rules given below in sections 9.7.11, 9.7.6, and 9.7.23.
The translator converts all RSL identifiers to unique SML identifiers, which start with the original identifier. This ensures both uniqueness and no clashes with SML reserved words. It is not intended that the SML code be readable or changeable by hand, nor that users need to know SML.
The translator produced code is intended for use with SML/NJ (SML of New Jersey), which is based on SML'97 [5]. The run-time system for SML/NJ is freely available for a variety of platforms from http://cm.bell-labs.com/cm/cs/what/smlnj/. The translator has been tested on Solaris, Linux and Windows 9X and NT.
The following lists mention known errors and problems.
The arithmetic types Int (including Nat) and Real are naively translated into Int and Real without regard for actual limits and precision.
The translation relies heavily on the syntactic form of the input, which means that often a semantically equivalent piece of RSL text cannot be translated or is translated differently. For example, a record or variant type is accepted, but the equivalent expansion into a sort, some value signatures, and some axioms is not accepted.
| 9.1 Introduction | ||||||
|
| |||||