We first discuss two ways to provide a special syntax for numbers. This results in a proposal of how to extend the CASL-Syntax and how to translate this extension back into standard CASL. Finally we demonstrate that the proposed extension on numbers fits with our specifications of numbers in [RM99].

There are basically two ways of providing a special syntax for natural numbers:

**First approach:**- Introduce a constant for each number, and
axiomatize the successor operation by providing one axiom for each
number.
The drawback of this approach is that the specification of natural numbers consists of an infinite signature and and infinite number of axioms. There is no difficulty in modifying the CASL semantics to allow such specifications. However, such infinite theories have to be hard-wired into theorem provers. This makes it more difficult to re-use existing theorem provers by building translations from CASL to tool-supported languages.

**Second approach:**- Translate a numeral into a sequence of digits.
Just translating a sequence of digits
*d*to_{1}d_{2}...d_{n}*d*would require to introduce the digits as prefix or postfix operations. However, this leads to the peculiarity that_{1}d_{2}... d_{n}*56 78*is the same as*5678*. Thus, a better way is to insert operation symbols between the digits. That is,*d*is translated to_{1}d_{2}...d_{n}*d*._{1}:: d_{2}:: ...:: d_{n}The drawback of this approach is that it is not possible to pass a multi-digit number directly as an actual parameter to a generic specification. Instead, one has to introduce an extension of the natural numbers, where the number is named as a constant, and pass this constant to the generic specification

^{8}.

We propose to adopt the second approach.

According to section C.4 of [CoF98] we suggest the following extended syntax for numbers:

Digit | ::= | 0 | 1 | ... | 9 |

Sign | ::= | + | - |

Number | ::= |
Digit |
Number Digit |

Fraction | ::= |
Number |
Number . Number |

Expo | ::= |
Fraction E Number
| |

Fraction E Sign Number | ||

*[ [ 0 ] ]:= 0,**[ [ 1 ] ]:= 1,*- ...
*[ [ 9 ] ]:= 9,**[ [ + ] ]:= +,**[ [ - ] ]:= -,**[ [*`&`nbsp;Number`&`nbsp;Digit ] ]:= [ [`&`nbsp;Number ] ] :: [ [`&`nbsp;Digit ] ],*[ [*and`&`nbsp;Number .`&`nbsp;Number ] ]:= [ [`&`nbsp;Number ] ] ::: [ [`&`nbsp;Number ] ] ,*[ [*where`&`nbsp;Fraction E`&`nbsp;Number ] ]:= [ [`&`nbsp;Fraction ] ] ' ' E ' ' [ [`&`nbsp;Number ] ],*' '*denotes a space.*[ [*where`&`nbsp;Fraction E`&`nbsp;Sign`&`nbsp;Number ] ]:= [ [`&`nbsp;Fraction ] ] ' ' E ' ' [ [`&`nbsp;Sign ] ] [ [`&`nbsp;Number ] ],*' '*denotes a space.

*0,**1,*...,*9,**+__,**-__,**__ :: __,**__ ::: __*, and*__ E __*

Natural numbers are represented in [RM99] as sequences of digits
*d _{1} :: d_{2}:: ...:: d_{n}*. This representation carries over to
integers, where we add a sign to the numbers, and rational numbers,
which are represented as a pair of an integer and a positive number.
For finite decimal fractions we provide a special notion, which makes
use of the operator

The representations of natural numbers is specified in [RM99] as follows:

**spec**- Nat =
- GenerateNat
**with****sorts***Nat, Pos,***ops***0, suc, pre* **then****...**-
**ops***1,2,3,4,5,6,7,8,9:**Nat;**__ :: __ :**Nat × Nat -> Nat %***left assoc****%%**- representing the natural numbers with digits:
**.**-
*1 = suc (0)* **.**-
*2 = suc (1)* **.**-
*3 = suc (2)* **.**-
*4 = suc (3)* **.**-
*5 = suc (4)* **.**-
*6 = suc (5)* **.**-
*7 = suc (6)* **.**-
*8 = suc (7)* **.**-
*9 = suc (8)* **.**-
*m :: n = (m * suc(9)) + n*

**end**

The syntax for integers is derived from the above syntax of natural
numbers by introducing *+* (unary) and *-* (unary) as operation
symbols:

**spec**- Int =
- GenerateInt
**with****sorts***Nat, Pos, Neg, Int***ops***0, suc, pre* **then****...**-
**ops***+__,**-__:**Int -> Int;*

**end**

The representation for rationals in [RM99] is obtained by
operators *+__* (unary), *-__* (unary), and *__/__* (binary):

**spec**- GenerateRat =
- Int ...
**then****free****{**-
**type***Rat ::=***sort**Int | __ / __ (nom: Int ; denom: Pos)**...**

**}****end**

**spec**- Rat =
- GenerateRat ...
**then****...**-
**ops***+ __ ,**- __ :**Rat -> Rat;*

**end**

For the representation of a subset of the rational numbers, the finite
decimal fractions, we further introduce operations *__:::__* and
*__E__* in [RM99]:

**spec**- Rat =
**...**-
**ops***__ ::: __ :**Nat × Nat -> Rat;**__ E __ :**Rat × Int -> Rat***vars***n,m: Nat; p: Pos***%%**- represent the floating point number
*n.m*as rational: **.**-
*n:::m = n + (m/tenPower(m))* **%%**- introduce an exponent:
**.**-
*r E n = r* ((1::0) ^ n)* **.**-
*r E (-p) = r / ((1::0) ^ n)*

**end**

The representation of the real numbers is the same as for rational
numbers resp. finite decimal fractions: in [MR99] the
**sort** *Real* is defined as supersort of *Rat*:

**spec**- DefineBasicReal =
- ArchimedianField[DefineArchimedianField]
**with***Elem*^{|}->*Real***and**Rat **then**-
**sort***Rat < Real***%%**- The embedding is determined by overloading of
*0,1,+,*_{,}*,/ **...**

**end**

**spec**- BasicReal[DefineBasicReal] =
**...****ops***pi,**e :**Real;***axioms**-
*e = exp(1)* -
*pi = 4*arcsin(sqrt(1/2))* **...****end**

Complex numbers are specified in [MR99] as pairs of two real
numbers. Thus again the representations for rational numbers
resp. finite decimal fractions carry over and there is no need for
further special syntax. The complex number *i* and the operator *__
i,* which denotes the imaginary part of a complex number, are obtained
by overloading.

**spec**- BasicComplex =
- BasicReal
**then**-
**free****type***Complex ::= c(real,imag: Real)***sorts***Real < Complex***ops***i :**Complex;**__ i :**Real -> Complex;**...***axiom**-
*i = c(0,1)* **var***x: Real***.**-
*x i = c(0,x)* **...**

**end**

CoFI Note: L-11 -- Version: 0.1 -- 11 March 1999.

Comments to roba@informatik.uni-bremen.de