Strings - Revision history

Michael Leuschel: /* LibraryRegex */

2026-07-10T12:27:39Z

LibraryRegex

← Older revision		Revision as of 12:27, 10 July 2026
Line 127:		Line 127:
	REGEX_REPLACE("ab12cd34","[0-9]+","($0)")		REGEX_REPLACE("ab12cd34","[0-9]+","($0)")
	ab(12)cd(34)		ab(12)cd(34)
	* <tt>REGEX_SEARCH_STR<tt> searches for the first occurence of a pattern in a string.		* <tt>REGEX_SEARCH_STR</tt> searches for the first occurence of a pattern in a string.
	REGEX_SEARCH_STR("abcdef000234daf","[1-9][0-9]*")		REGEX_SEARCH_STR("abcdef000234daf","[1-9][0-9]*")
	"234"		"234"

Michael Leuschel: /* LibraryStrings */

2026-07-10T12:27:14Z

LibraryStrings

← Older revision		Revision as of 12:27, 10 July 2026
Line 47:		Line 47:
	DEFINITIONS "LibraryStrings.def"		DEFINITIONS "LibraryStrings.def"

	The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib</tt> folder. You can also include the machine <tt>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).		The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib</tt> folder. You can also include the machine <tt>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:		Below are a few of the provided external functions along with some example uses:

Michael Leuschel: /* LibraryStrings */

2026-07-10T12:27:00Z

LibraryStrings

← Older revision		Revision as of 12:27, 10 July 2026
Line 47:		Line 47:
	DEFINITIONS "LibraryStrings.def"		DEFINITIONS "LibraryStrings.def"

	The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib<\tt> folder. You can also include the machine <tt>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).		The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib</tt> folder. You can also include the machine <tt>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:		Below are a few of the provided external functions along with some example uses:

Michael Leuschel: /* LibraryStrings */

2026-07-10T12:24:51Z

LibraryStrings

← Older revision		Revision as of 12:24, 10 July 2026
Line 45:		Line 45:

	You can obtain the definitions of this library by putting the following into your DEFINITIONS clause:		You can obtain the definitions of this library by putting the following into your DEFINITIONS clause:
			DEFINITIONS "LibraryStrings.def"
	`DEFINITIONS "LibraryStrings.def"`

	The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib<\tt> folder. You can also include the machine <tt>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).		The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib<\tt> folder. You can also include the machine <tt>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).

Michael Leuschel: /* LibraryStrings */

2026-07-10T12:24:25Z

LibraryStrings

← Older revision		Revision as of 12:24, 10 July 2026
Line 48:		Line 48:
	`DEFINITIONS "LibraryStrings.def"`		`DEFINITIONS "LibraryStrings.def"`

	The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib<\tt> folder.		The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib<\tt> folder. You can also include the machine <tt>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).
	You can also include the machine <tt>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:		Below are a few of the provided external functions along with some example uses:
Line 96:		Line 95:
	* <tt>FORMAT_TO_STRING</tt> 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.		* <tt>FORMAT_TO_STRING</tt> 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.
	* <tt>STRINGIFY</tt> 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).		* <tt>STRINGIFY</tt> 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).
			* <tt>STRING_REPLACE</tt> replaces a pattern within a string by another string.
			STRING_REPLACE("a.bc.d",".","->")
			"a->bc->d"
			* <tt>STRING_TO_REAL</tt> convert string to a real number.
			* <tt>STRING_REV</tt> reverses a string, equivalent to rev(.) unary operator.
			* <tt>STRING_CONC</tt> takes a sequence of strings and concatenates them. Equivalent to conc(.) unary operator.

	=== LibraryRegex ===		=== LibraryRegex ===

Michael Leuschel: /* LibraryRegex */

2026-07-10T10:13:16Z

LibraryRegex

← Older revision		Revision as of 10:13, 10 July 2026
Line 100:		Line 100:

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

			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 <tt>LibraryRegex.def</tt> is also bundled with ProB and can be found in the <tt>stdlib</tt> 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: [http://www.cplusplus.com/reference/regex/ECMAScript/].
			The library is currently implemented using the C++ standard library.
			Below we repeat some information from [http://www.cplusplus.com/reference/regex/ECMAScript/] 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.

			* <tt>REGEX_MATCH</tt> 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
			* <tt>IS_REGEXP</tt> is a predicate which checks if a string is a valid regular expression pattern.
			* <tt>REGEXP_REPLACE</tt> 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)
			* <tt>REGEX_SEARCH_STR<tt> searches for the first occurence of a pattern in a string.
			REGEX_SEARCH_STR("abcdef000234daf","[1-9][0-9]*")
			"234"
			* <tt>REGEX_SEARCH</tt> 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:∅)
			* <tt>REGEX_SEARCH_ALL</tt> 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"

Michael Leuschel: /* LibraryStrings */

2026-07-10T10:02:44Z

LibraryStrings

@@ Line 62: / Line 62: @@
   STRING_SPLIT("usr/local/lib","/")
   {(1↦"usr"),(2↦"local"),(3↦"lib")}
-* <tt>STRING_JOIN</tt> takes a sequence of strings and a separator string
+* <tt>STRING_JOIN</tt> 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 <tt>STRING_SPLIT</tt> function.
   STRING_JOIN(["usr","local","lib"],"/")
@@ Line 75: / Line 74: @@
 * <tt>STRING_TO_LOWER</tt> 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).
 * <tt>STRING_EQUAL_CASE_INSENSITIVE</tt> compares two strings ignoring lower/upper case distinctions and diacritical marks. It works as if converting the strings using <tt>STRING_TO_UPPER</tt> before comparing.
-* <tt>INT_TO_STRING</tt>,...
+ STRING_EQUAL_CASE_INSENSITIVE("aOuB","AoUB")
 === LibraryRegex ===
 <tt>LibraryRegex.def</tt>: providing access to regular expression operators on strings (<tt>REGEX_MATCH</tt>, <tt>REGEX_REPLACE</tt>, <tt>REGEX_SEARCH</tt>,...)

Michael Leuschel: /* LibraryStrings */

2026-07-10T09:27:33Z

LibraryStrings

← Older revision		Revision as of 09:27, 10 July 2026
Line 49:		Line 49:

	The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib<\tt> folder.		The file <tt>LibraryStrings.def</tt> is bundled with ProB and can be found in the <tt>stdlib<\tt> folder.
	You can also include the machine <tt>LibraryStrings.mch<\tt> instead of the definition file;		You can also include the machine <tt>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).
	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:		Below are a few of the provided external functions along with some example uses:
Line 62:		Line 59:
	STRING_LENGTH("abc")		STRING_LENGTH("abc")
	3		3
	* <tt>STRING_SPLIT</tt> takes two strings and separates the first string		* <tt>STRING_SPLIT</tt> takes two strings and separates the first string according to the separator specified by the second string:
	according to the separator specified by the second string:
	STRING_SPLIT("usr/local/lib","/")		STRING_SPLIT("usr/local/lib","/")
	{(1↦"usr"),(2↦"local"),(3↦"lib")}		{(1↦"usr"),(2↦"local"),(3↦"lib")}

Michael Leuschel: /* LibraryStrings */

2026-07-10T09:27:00Z

LibraryStrings

← Older revision		Revision as of 09:27, 10 July 2026
Line 71:		Line 71:
	STRING_JOIN(["usr","local","lib"],"/")		STRING_JOIN(["usr","local","lib"],"/")
	"usr/local/lib"		"usr/local/lib"
	* <tt>STRING_CHARS</tt> takes a strings splits it into a sequence		* <tt>STRING_CHARS</tt> takes a strings splits it into a sequence of the individual characters. Each character is represented by a string.
	of the individual characters. Each character is represented by a string.		* <tt>STRING_CODES</tt> 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).
	* <tt>STRING_CODES</tt> 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).
	* <tt>CODES_TO_STRING</tt> is the inverse of the <tt>STRING_CODES</tt> function above		* <tt>CODES_TO_STRING</tt> is the inverse of the <tt>STRING_CODES</tt> function above
	CODES_TO_STRING([65,66,67])		CODES_TO_STRING([65,66,67])

Michael Leuschel: /* LibraryStrings */

2026-07-10T09:26:13Z

LibraryStrings

@@ Line 44: / Line 44: @@
 === LibraryStrings ===
-<tt>LibraryStrings.def</tt> used by <tt>LibraryStrings.mch</tt>: providing direct access to various operators on strings (<tt>STRING_LENGTH</tt>, <tt>STRING_APPEND</tt>, <tt>STRING_SPLIT</tt>, <tt>INT_TO_STRING</tt>,...)
+You can obtain the definitions of this library by putting the following into your DEFINITIONS clause:
 === LibraryRegex ===
 <tt>LibraryRegex.def</tt>: providing access to regular expression operators on strings (<tt>REGEX_MATCH</tt>, <tt>REGEX_REPLACE</tt>, <tt>REGEX_SEARCH</tt>,...)