Strings
Strings: Concepts, Issues, and Designs
Note: STRING is a primeval (or: built-in) spec: you can refer to the sort
String and the various operations, but you cannot refer to the STRING spec
itself.
String literals
Within Strings, there are two characters with special meaning that require
a backslash (ie. '\')
to escape from their special meaning: '"' and '\'.
Hence, the appropriate string
literals are "\"" and "\\" Also, within strings, the two nonprinting Chars
space and newline can be used directly: " " and "
".
String spec:
string.re
STRING is essentially a recursive sum, but is expressed via subtypes.
- Sorts
-
String
NE-String
Defined-Dom-String
- Constructors
-
empty-string
prepend-string
- Testors
-
empty-string?
nonempty-string?
- Destructors
-
first-string
rest-string
- Operations
-
append-string
singleton-string
concat-string
size-string
lt-string
leq-string
gt-string
geq-string
valid-index-string
apply-string
SpecWeb Index
Specs