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