5.3 Extended Syntax for Characters and Strings

Our specification of characters in [RM99] assumes that a certain list of names delimited by single quotes are available as identifiers:

spec

Char =

Nat

then

sort

Char

preds

isLetter, isDigit, isPrintable: Char

ops

chr : Nat ->? Char;

ord : Char -> Nat;

vars

n:Nat; c:Char

...

%%

Characters c with 32 < ord(c) < 160:

op

' ' : Char; axiom ord(' ') = 32;

...

op

' ~ ' : Char; axiom ord(' ~ ') = 126;

%%

and all Characters c with 161 < ord(c) < 255:

op

' ' : Char; axiom ord(' ') = 160;

...

op

'ÿ' : Char; axiom ord('ÿ') = 255;

...

%%

alternative definition of characters as ' \ nnn':

op

' \ 000' : Char; axiom ord(' \ 000') = 0;

...

op

' \ 255' : Char; axiom ord(' \ 255') = 255;

end

The list comprises of 'c', where c is any printing character except one of the three characters ', " and \. These characters are represented as '\' ', '\" ', and '\\'. Further on this list consists of elements ' \ nnn', where nnn is a numeral in the range from 0 to 255.

The specification of strings in [RM99] again assumes a special syntax for characters and lists. For strings (i.e. lists of characters) we assume the following special syntax: The empty string "" is allowed as an identifier. Moreover, a string "c₁ ...c_n" is parsed as 'c₁':: ...:: 'c_n' :: "", where the 'c_i' are operation names from the specification Char and the operation :: inserts a character in a list. This leads to the specification:

spec

String =

List

[Char] with sorts List[Char] |-> String, NonEmptyList[Char] |-> NonEmptyString, preds isEmpty, ops __::__, last, length, __ + + __, reverse, take, drop, nil |-> ""

end