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

LibraryStrings.def used by LibraryStrings.mch: providing direct access to various operators on strings (STRING_LENGTH, STRING_APPEND, STRING_SPLIT, INT_TO_STRING,...)

LibraryRegex

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