Strings

ProB supports the STRING data type also provided by Atelier-B. However, ProB provides considerable additional features described below.

Literals

 "astring"      a specific (single-line) string value
 '''astring'''  an alternate way of writing (multi-line) strings, no need to escape "
 ```tstring```  template strings, where ${Expr} or $«Expr» parts are evaluated and converted to string,
                you can provide options separated by commas in square brackets like $[2f]{Expr}.
                Valid options are: Nf (for floats/reals), Nd (for integer), Np (padding),
                ascii (can be abbreviated to a), unicode (can be abbreviated to u).

Escaping and Encoding

ProB supports the following escape sequences within strings:

\n  newline (ASCII character 13)
\r  carriage return (ASCII 10)
\t  tab (ASCII 9)
\"  the double quote symbol "
\'  the single quote symbol '
\\  the backslash symbol

Within single-line string literals, you do not need to escape '. Within multi-line string literals, you do not need to escape " and you can use tabs and newlines.

ProB assumes that all B machines and strings use the UTF-8 encoding.

Operators

Atelier-B does not support any operations on strings, apart from equality and disequality. In ProB, however, some of the sequence operators work also on strings:

size(s)   the length of a string s
rev(s)    the reverse of a string s
s ^ t     the concatenation of two strings
conc(ss)  the concatenation of a sequence of strings

You can turn this support off using the STRING_AS_SEQUENCE preference.

External Functions

ProB provides various external functions to manipulate strings.

LibraryStrings

You can obtain the definitions of this library by putting the following into your DEFINITIONS clause:

`DEFINITIONS "LibraryStrings.def"`

The file LibraryStrings.def is bundled with ProB and can be found in the stdlib<\tt> folder. You can also include the machine LibraryStrings.mch<\tt> instead of the definition file;

the machine defines some of the functions below as proper B functions (i.e., functions
for which you can compute the domain and use constructs such as
relational image).

Below are a few of the provided external functions along with some example uses:

• STRING_APPEND takes two strings and concatenates them:

STRING_APPEND("abc","abc")
"abcabc"

• STRING_LENGTH takes a string and returns the length:

STRING_LENGTH("abc")
3

• STRING_SPLIT takes two strings and separates the first string

according to the separator specified by the second string:
STRING_SPLIT("usr/local/lib","/")
{(1↦"usr"),(2↦"local"),(3↦"lib")}

• STRING_JOIN takes a sequence of strings and a separator string

and joins the strings together inserting the separators as often as needed.

It is the inverse of the STRING_SPLIT function.

STRING_JOIN(["usr","local","lib"],"/")
"usr/local/lib"

• STRING_CHARS takes a strings splits it into a sequence

of the individual characters. Each character is represented by a string.

• STRING_CODES takes a string and splits it into a sequence

of the individual characters. Each character is represented by a natural number

(the ASCII or Unicode representation of the character).

• CODES_TO_STRING is the inverse of the STRING_CODES function above

CODES_TO_STRING([65,66,67])
"ABC"

• STRING_TO_UPPER converts a string to upper-case letters. It currently converts also diacritical marks (this behaviour may in future be controlled by an additional flag or option).
• STRING_TO_LOWER converts a string to lower-case letters. It currently converts also diacritical marks (this behaviour may in future be controlled by an additional flag or option).
• STRING_EQUAL_CASE_INSENSITIVE compares two strings ignoring lower/upper case distinctions and diacritical marks. It works as if converting the strings using STRING_TO_UPPER before comparing.
• INT_TO_STRING,...

LibraryRegex

LibraryRegex.def: providing access to regular expression operators on strings (REGEX_MATCH, REGEX_REPLACE, REGEX_SEARCH,...)