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 folder. You can also include the machine LibraryStrings.mch 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).
• STRING_REPLACE replaces a pattern within a string by another string.

STRING_REPLACE("a.bc.d",".","->")
"a->bc->d"

• STRING_TO_REAL convert string to a real number.
• STRING_REV reverses a string, equivalent to rev(.) unary operator.
• STRING_CONC takes a sequence of strings and concatenates them. Equivalent to conc(.) unary operator.

LibraryRegex

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

This library provides various facilities for pattern matching with regular expressions. You can obtain the definitions below by putting the following into your DEFINITIONS clause:

DEFINITIONS "LibraryRegex.def"

The file LibraryRegex.def is also bundled with ProB and can be found in the stdlib folder (as of version 1.8.3-beta4).

The library works on B strings and regular expression patterns are also written as B strings. The syntax used is the ECMAScript syntax: [1]. The library is currently implemented using the C++ standard library. Below we repeat some information from [2] for convenience.

The library now does support UTF-8 encoded strings and patterns. Note that ProB only supports UTF-8 for B machines and for any strings and Unicode files it processes.

• REGEX_MATCH is a predicate which checks if a string matches a regular expression pattern. For example, the following calls check whether the first argument is a non-empty sequenze of lower-case letters:

REGEX_MATCH("abc","[a-z]+")
TRUE

• IS_REGEXP is a predicate which checks if a string is a valid regular expression pattern.
• REGEXP_REPLACE replaces all occurences of a pattern in a string by a given replacement string. Note that you can use ```$1```, ```$2```, ... to refer to subgroups in the replacement string and ```$0``` to refer to the full match:

REGEX_REPLACE("a01b23c4d56","[0-9]+","NUM")
"aNUMbNUMcNUMdNUM"
REGEX_REPLACE("1abd00abc2","([a-z]+).*?([a-z]+)","<<$2$1>>")
1<<abcabd>>2
REGEX_REPLACE("ab12cd34","[0-9]+","($0)")
ab(12)cd(34)

• REGEX_SEARCH_STR searches for the **first** occurence of a pattern in a string.

REGEX_SEARCH_STR("abcdef000234daf","[1-9][0-9]*")
"234"

• REGEX_SEARCH searches for the first occurence of a pattern in a string and returns full information about the match: position, length, match and sub-matches. It also expects an index at which to start the search; which can be useful for writing loops to find all matches.

REGEX_SEARCH("abcdef000234daf",1,"alpha:+")
rec(length:6,position:1,string:"abcdef",submatches:∅)

• REGEX_SEARCH_ALL searches for the **all** occurence of a pattern in a string and returns the matched strings as a B sequence. It always starts to match at the beginning.

REGEX_SEARCH_ALL("abcdef000234daf567","([1-9])([0-9]*)")
{(1↦"234"),(2↦"567")}

As of ProB 1.12.0 the above functions also have counterparts which ignore the case. The names of the functions have and additional I (for Ignore case). Here are a few examples to illustrate their behaviour.

REGEX_IMATCH("abC","(a|b|c)+")
TRUE
REGEX_ISEARCH("abCabCdABC",1,"(a|b|c)+")'string
"abCabC"
REGEX_ISEARCH_STR("abCabCdABC","(a|b|c)+")
"abCabC"
REGEX_ISEARCH_ALL("abCabCdABC","(a|b|c)+")
{(1↦"abCabC"),(2↦"ABC")}
REGEX_IREPLACE("abCabCdABC","(a|b|c)+","*")
"*d*"