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.

STRING_EQUAL_CASE_INSENSITIVE("aOuB","AoUB")
TRUE

• SUB_STRING takes a strings a position and a sequence and produces a corresponding substring. The numbering starts at 1 and the position must be at least 1, but can extend beyond the end of the string.

SUB_STRING("abcdefg",1,3)
"abc"

• STRING_IS_INT takes a string and is true if the string represents an integer.
• STRING_TO_INT takes a string and converts it into an integer. An error is raised if this cannot be done. It is safer to first check with `STRING_IS_INT` whether the conversion can be done.
• INT_TO_STRING converts an integer to a string representation.
• DEC_STRING_TO_INT takes a decimal string (with optional decimal places) and converts it to an integer with the given precision (rounding if required).

DEC_STRING_TO_INT("1024",2)
102400

• INT_TO_DEC_STRING converts an integer to a decimal string representation with the precision provided by the second argument.
• INT_TO_HEX_STRING converts an integer to a hexadecimal string representation.
• STRING_IS_DECIMAL takes a string and is true if the string represents a decimal number. It requires a decimal point and digits both before and after the decimal point.
• STRING_IS_ALPHANUMERIC takes a string and is true if the string is non empty and contains only alphanumeric letters (a-z,A-Z,0-9) and nothing else.
• STRING_IS_NUMBER takes a string and is true if the string represents a number.
• STRING_PADLEFT adds a padding character at the left of a string if the size of the string is below the argument given.

STRING_PADLEFT("10",5,"0")
"00010"

• TO_STRING converts a B data value to a string representation.
• FORMAT_TO_STRING takes a format string and a B sequence of values and generates an output string, where the values have been inserted into the format string in place of the `~w` placeholders. The length of sequence must correspond to the number of `~w` in the format string. The format string follows the conventions of SICStus Prolog. E.g., one can use `~n` for newlines.
• STRINGIFY converts a B expression to a string representation of the expression, not the value. It can be used to obtain the name of variables. Warning: ProB may simplify and rewrite expressions (you can turn this off by setting the OPTIMIZE_AST preference to false).

LibraryRegex

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