Chars


Chars: Concepts, Issues, and Designs

Note: CHAR is a primeval (or: built-in) spec: you can refer to the sort Char and the various operations, but you cannot refer to the CHAR spec itself.

Char literals
The syntax for Char literals is '<char>' I.e., a Char delimited by two apostrophes (apostrophe is ASCII 39). For example, 'c' is the Char literal notation for a lower case c and 'C' is the notation for an upper case C. There are two characters with special meaning that require a backslash (ie. '\') to escape from their special meaning: @ and \ Hence, the appropriate literals are '\@' and '\\'. The current version (Specware 2.0) has literals notation for all the printing chars and the two nonprinting chars: space and newline. Note that the char literal notation for space is ' ' and for newline is '
'



CHAR spec: char.re

Char/Nat Conversions
There is an injection (char-to-nat) from Char to Nat and a partial inverse (nat-to-char) from the Nats less than max-char-code. Note that these conversions must agree with the ASCII ordering: char-to-nat must produce the ASCII code for a Char.
Predicates on char
There are four predicates: digit-char?, lower-char?, upper-char?, and alpha-char?
Ordering Relations
The ordering is the ASCII ordering. There are four ordering relations: lt-char, gt-char, leq-char, and geq-char,

SpecWeb Index Specs