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