Skip to content
Snippets Groups Projects
Commit fc5bedd1 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

fix typos

parent 336518a2
No related branches found
No related tags found
No related merge requests found
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# External Functions # External Functions
## LibraryStrings ## LibraryStrings
In pure B there are only two built-in operators on strings: equality $=$ and inequality $\neq$. In pure B there are only two built-in operators on strings: equality $=$ and inequality $\neq$.
This library provides several string manipulation functions, and assumes that STRINGS are This library provides several string manipulation functions, and assumes that STRINGS are
sequences of unicode characters (in UTF-8 encoding). sequences of unicode characters (in UTF-8 encoding).
You can obtain the definitions below by putting the following into your DEFINITIONS clause: You can obtain the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "LibraryStrings.def"` `DEFINITIONS "LibraryStrings.def"`
The file `LibraryStrings.def` is bundled with ProB and can be found in the `stdlib` folder. 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; 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 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 for which you can compute the domain and use constructs such as
relational image). relational image).
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Jupyter MACHINE Jupyter
DEFINITIONS // "LibraryStrings.def" DEFINITIONS // "LibraryStrings.def"
STRING_LENGTH(xxx) == length(xxx); STRING_LENGTH(xxx) == length(xxx);
EXTERNAL_FUNCTION_STRING_LENGTH == STRING --> INTEGER; EXTERNAL_FUNCTION_STRING_LENGTH == STRING --> INTEGER;
/* This external function takes two strings and concatenates them. */ /* This external function takes two strings and concatenates them. */
STRING_APPEND(xxx,yyy) == append(xxx,yyy); STRING_APPEND(xxx,yyy) == append(xxx,yyy);
EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING; EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;
/* This external function takes a sequence of strings and concatenates them. */ /* This external function takes a sequence of strings and concatenates them. */
STRING_CONC(string_conc_list) == ""; STRING_CONC(string_conc_list) == "";
EXTERNAL_FUNCTION_STRING_CONC == seq(STRING) --> STRING; EXTERNAL_FUNCTION_STRING_CONC == seq(STRING) --> STRING;
/* This external function takes two strings and separates the first string /* This external function 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(xxx,yyy) == split(xxx,yyy); STRING_SPLIT(xxx,yyy) == split(xxx,yyy);
EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING)); EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));
/* This external function takes a sequence of strings and a separator string /* This external function takes a sequence of strings and a separator string
and joins the strings together inserting the separators as often as needed. and joins the strings together inserting the separators as often as needed.
It is the inverse of the STRING_SPLIT function. */ It is the inverse of the STRING_SPLIT function. */
STRING_JOIN(xxx,yyy) == join(xxx,yyy); STRING_JOIN(xxx,yyy) == join(xxx,yyy);
EXTERNAL_FUNCTION_STRING_JOIN == (((INTEGER<->STRING)*STRING) --> STRING); EXTERNAL_FUNCTION_STRING_JOIN == (((INTEGER<->STRING)*STRING) --> STRING);
STRING_CHARS(xxx) == chars(xxx); STRING_CHARS(xxx) == chars(xxx);
EXTERNAL_FUNCTION_STRING_CHARS == (STRING --> (INTEGER<->STRING)); EXTERNAL_FUNCTION_STRING_CHARS == (STRING --> (INTEGER<->STRING));
STRING_CODES(xxx) == codes(xxx); STRING_CODES(xxx) == codes(xxx);
EXTERNAL_FUNCTION_STRING_CODES == (STRING --> (INTEGER<->INTEGER)); EXTERNAL_FUNCTION_STRING_CODES == (STRING --> (INTEGER<->INTEGER));
/* This external function takes a string and converts it into an integer. /* This external function takes a string and converts it into an integer.
An error is raised if this cannot be done. An error is raised if this cannot be done.
It is safer to first check with {\tt STRING\_IS\_INT} whether the conversion can be done. */ It is safer to first check with {\tt STRING\_IS\_INT} whether the conversion can be done. */
STRING_TO_INT(sss) == 0; STRING_TO_INT(sss) == 0;
EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER); EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER);
/* This external predicate takes a string and is true if the string represents an integer. */ /* This external predicate takes a string and is true if the string represents an integer. */
STRING_IS_INT(sss) == (1=1); STRING_IS_INT(sss) == (1=1);
EXTERNAL_PREDICATE_STRING_IS_INT == (STRING); EXTERNAL_PREDICATE_STRING_IS_INT == (STRING);
/* This external function takes a decimal string (with optional decimal places) /* This external function takes a decimal string (with optional decimal places)
and converts it to an integer with the given precision. */ and converts it to an integer with the given precision. */
EXTERNAL_FUNCTION_DEC_STRING_TO_INT == STRING * INTEGER --> INTEGER; EXTERNAL_FUNCTION_DEC_STRING_TO_INT == STRING * INTEGER --> INTEGER;
DEC_STRING_TO_INT(decimal_string,precision) == 0; DEC_STRING_TO_INT(decimal_string,precision) == 0;
/* parametric function; cannot be represented as constant function : */ /* parametric function; cannot be represented as constant function : */
STRING_TO_ENUM(sss) ==({}(1)); /* Note: you have to include the DEFINITION into your B file */ STRING_TO_ENUM(sss) ==({}(1)); /* Note: you have to include the DEFINITION into your B file */
EXTERNAL_FUNCTION_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == (STRING --> STRING_TO_ENUM_TYPE); EXTERNAL_FUNCTION_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == (STRING --> STRING_TO_ENUM_TYPE);
TYPED_STRING_TO_ENUM(t,sss) ==({}(1)); TYPED_STRING_TO_ENUM(t,sss) ==({}(1));
EXTERNAL_FUNCTION_TYPED_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == EXTERNAL_FUNCTION_TYPED_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) ==
(POW(STRING_TO_ENUM_TYPE)*STRING --> STRING_TO_ENUM_TYPE); (POW(STRING_TO_ENUM_TYPE)*STRING --> STRING_TO_ENUM_TYPE);
/* This external function converts an integer to a string representation. */ /* This external function converts an integer to a string representation. */
INT_TO_STRING(sss) == "0"; INT_TO_STRING(sss) == "0";
EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING); EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING);
/* This external function converts an integer to a decimal string representation /* This external function converts an integer to a decimal string representation
with the precision provided by the second argument. */ with the precision provided by the second argument. */
INT_TO_DEC_STRING(integer,precision) == "0.0"; INT_TO_DEC_STRING(integer,precision) == "0.0";
EXTERNAL_FUNCTION_INT_TO_DEC_STRING == (INTEGER*INTEGER --> STRING); EXTERNAL_FUNCTION_INT_TO_DEC_STRING == (INTEGER*INTEGER --> STRING);
/* This external function converts a B data value to a string representation. */ /* This external function converts a B data value to a string representation. */
TO_STRING(sss) == "0"; TO_STRING(sss) == "0";
EXTERNAL_FUNCTION_TO_STRING(TO_STRING_TYPE) == (TO_STRING_TYPE --> STRING); EXTERNAL_FUNCTION_TO_STRING(TO_STRING_TYPE) == (TO_STRING_TYPE --> STRING);
/* This external function takes a format string and a B sequence of values and generates an output /* This external function 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. string, where the values have been inserted into the format string in place of the ~w placeholders.
*/ */
FORMAT_TO_STRING(MyFormatString,ListOfValues) == "0"; FORMAT_TO_STRING(MyFormatString,ListOfValues) == "0";
EXTERNAL_FUNCTION_FORMAT_TO_STRING(FORMAT_TO_STRING_TYPE) == ((STRING*seq(FORMAT_TO_STRING_TYPE)) --> STRING); EXTERNAL_FUNCTION_FORMAT_TO_STRING(FORMAT_TO_STRING_TYPE) == ((STRING*seq(FORMAT_TO_STRING_TYPE)) --> STRING);
/* This external function checks whether the second string occurs contiguously within the first string. */ /* This external function checks whether the second string occurs contiguously within the first string. */
EXTERNAL_FUNCTION_STRING_CONTAINS_STRING == (STRING*STRING)--> BOOL; EXTERNAL_FUNCTION_STRING_CONTAINS_STRING == (STRING*STRING)--> BOOL;
STRING_CONTAINS_STRING(arg1,arg2)==FALSE; // TRUE when arg2 occurs as contiguous substring in arg1 STRING_CONTAINS_STRING(arg1,arg2)==FALSE; // TRUE when arg2 occurs as contiguous substring in arg1
END END
``` ```
%% Output %% Output
[2018-05-11 13:21:44,730, T+246558] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh [2018-05-11 13:21:44,730, T+246558] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-11 13:21:45,901, T+247729] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62905 [2018-05-11 13:21:45,901, T+247729] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62905
[2018-05-11 13:21:45,901, T+247729] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 40975 [2018-05-11 13:21:45,901, T+247729] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 40975
[2018-05-11 13:21:45,904, T+247732] "ProB Output Logger for instance 342c2add" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop -- [2018-05-11 13:21:45,904, T+247732] "ProB Output Logger for instance 342c2add" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-11 13:21:45,926, T+247754] "ProB Output Logger for instance 342c2add" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1 [2018-05-11 13:21:45,926, T+247754] "ProB Output Logger for instance 342c2add" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-11 13:21:46,041, T+247869] "ProB Output Logger for instance 342c2add" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/tests]) [2018-05-11 13:21:46,041, T+247869] "ProB Output Logger for instance 342c2add" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/tests])
Loaded machine: Jupyter : [] Loaded machine: Jupyter : []
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_APPEND ### STRING_APPEND
This external function takes two strings and concatenates them. This external function takes two strings and concatenates them.
Type: $STRING \times STRING \rightarrow STRING $. Type: $STRING \times STRING \rightarrow STRING $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_APPEND("abc","abc") STRING_APPEND("abc","abc")
``` ```
%% Output %% Output
"abcabc" "abcabc"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_APPEND("abc","") STRING_APPEND("abc","")
``` ```
%% Output %% Output
"abc" "abc"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_LENGTH ### STRING_LENGTH
This external function takes a string and returns the length. This external function takes a string and returns the length.
Type: $STRING \rightarrow INTEGER$. Type: $STRING \rightarrow INTEGER$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_LENGTH("abc") STRING_LENGTH("abc")
``` ```
%% Output %% Output
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_LENGTH("") STRING_LENGTH("")
``` ```
%% Output %% Output
0 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_SPLIT ### STRING_SPLIT
This external function takes two strings and separates the first string This external function 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.
Type: $STRING \times STRING \rightarrow \mathit{seq}(STRING) $. Type: $STRING \times STRING \rightarrow \mathit{seq}(STRING) $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_SPLIT("filename.ext",".") STRING_SPLIT("filename.ext",".")
``` ```
%% Output %% Output
{(1↦"filename"),(2↦"ext")} {(1↦"filename"),(2↦"ext")}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_SPLIT("filename.ext","/") STRING_SPLIT("filename.ext","/")
``` ```
%% Output %% Output
{(1↦"filename.ext")} {(1↦"filename.ext")}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_SPLIT("usr/local/lib","/") STRING_SPLIT("usr/local/lib","/")
``` ```
%% Output %% Output
["usr","local","lib"] ["usr","local","lib"]
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_SPLIT("",".") STRING_SPLIT("",".")
``` ```
%% Output %% Output
{(1↦"")} {(1↦"")}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
I am not sure the following result makes sense, maybe a sequence of all characters is more appropriate? I am not sure the following result makes sense, maybe a sequence of all characters is more appropriate?
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_SPLIT("usr/local/lib","") STRING_SPLIT("usr/local/lib","")
``` ```
%% Output %% Output
{(1↦"usr/local/lib")} {(1↦"usr/local/lib")}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_SPLIT("usr/local/lib","cal") STRING_SPLIT("usr/local/lib","cal")
``` ```
%% Output %% Output
{(1↦"usr/lo"),(2↦"/lib")} {(1↦"usr/lo"),(2↦"/lib")}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_JOIN ### STRING_JOIN
This external function takes a sequence of strings and a separator string This external function takes a sequence of strings and a separator string
and joins the strings together inserting the separators as often as needed. and joins the strings together inserting the separators as often as needed.
It is the inverse of the `STRING_SPLIT` function. It is the inverse of the `STRING_SPLIT` function.
Type: $\mathit{seq}(STRING) \times STRING \rightarrow STRING $. Type: $\mathit{seq}(STRING) \times STRING \rightarrow STRING $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_JOIN(["usr","local","lib"],"/") STRING_JOIN(["usr","local","lib"],"/")
``` ```
%% Output %% Output
"usr/local/lib" "usr/local/lib"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_JOIN(["usr/lo","/lib"],"cal") STRING_JOIN(["usr/lo","/lib"],"cal")
``` ```
%% Output %% Output
"usr/local/lib" "usr/local/lib"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_JOIN(["usr/local/lib"],"") STRING_JOIN(["usr/local/lib"],"")
``` ```
%% Output %% Output
"usr/local/lib" "usr/local/lib"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_CHARS ### STRING_CHARS
This external function takes a strings splits it into a sequence This external function 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.
Type: $STRING \rightarrow \mathit{seq}(STRING) $. Type: $STRING \rightarrow \mathit{seq}(STRING) $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_CHARS("") STRING_CHARS("")
``` ```
%% Output %% Output
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_CHARS("abc") STRING_CHARS("abc")
``` ```
%% Output %% Output
["a","b","c"] ["a","b","c"]
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_JOIN(STRING_CHARS("abc"),".") STRING_JOIN(STRING_CHARS("abc"),".")
``` ```
%% Output %% Output
"a.b.c" "a.b.c"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_CODES ### STRING_CODES
This external function takes a strings splits it into a sequence This external function takes a strings splits it into a sequence
of the individual characters. Each character is represented by a natural number of the individual characters. Each character is represented by a natural number
(the ASCII or Unicode representation of the character). (the ASCII or Unicode representation of the character).
Type: $STRING \rightarrow \mathit{seq}(INTEGER) $. Type: $STRING \rightarrow \mathit{seq}(INTEGER) $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_CODES("") STRING_CODES("")
``` ```
%% Output %% Output
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_CODES("AZ az 09") STRING_CODES("AZ az 09")
``` ```
%% Output %% Output
[65,90,32,97,122,32,48,57] [65,90,32,97,122,32,48,57]
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_IS_INT ### STRING_IS_INT
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
This external predicate takes a string and is true if the string represents an integer. This external predicate takes a string and is true if the string represents an integer.
Type: $STRING $. Type: $STRING $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("1204") STRING_IS_INT("1204")
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("-1204") STRING_IS_INT("-1204")
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT(" - 1204") STRING_IS_INT(" - 1204")
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("1.1") STRING_IS_INT("1.1")
``` ```
%% Output %% Output
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("1.0") STRING_IS_INT("1.0")
``` ```
%% Output %% Output
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("a") STRING_IS_INT("a")
``` ```
%% Output %% Output
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("1000000000000000000000000000") STRING_IS_INT("1000000000000000000000000000")
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("-00001") STRING_IS_INT("-00001")
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_IS_INT("00002") STRING_IS_INT("00002")
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### STRING_TO_INT ### STRING_TO_INT
This external function takes a string and converts it into an integer. This external function takes a string and converts it into an integer.
An error is raised if this cannot be done. 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. It is safer to first check with `STRING_IS_INT` whether the conversion can be done.
Type: $STRING \rightarrow INTEGER$. Type: $STRING \rightarrow INTEGER$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_TO_INT("1024") STRING_TO_INT("1024")
``` ```
%% Output %% Output
1024 1024
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_TO_INT(" - 00001") STRING_TO_INT(" - 00001")
``` ```
%% Output %% Output
−1 −1
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### INT_TO_STRING ### INT_TO_STRING
This external function converts an integer to a string representation. This external function converts an integer to a string representation.
Type: $INTEGER \rightarrow STRING $. Type: $INTEGER \rightarrow STRING $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_STRING(1024) INT_TO_STRING(1024)
``` ```
%% Output %% Output
"1024" "1024"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_STRING(-1024) INT_TO_STRING(-1024)
``` ```
%% Output %% Output
"-1024" "-1024"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_STRING(STRING_TO_INT(" - 00001")) INT_TO_STRING(STRING_TO_INT(" - 00001"))
``` ```
%% Output %% Output
"-1" "-1"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
STRING_TO_INT(INT_TO_STRING(-1))=-1 STRING_TO_INT(INT_TO_STRING(-1))=-1
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### DEC_STRING_TO_INT ### DEC_STRING_TO_INT
This external function takes a decimal string (with optional decimal places) and converts it to an integer with the given precision (rounding if required). This external function takes a decimal string (with optional decimal places) and converts it to an integer with the given precision (rounding if required).
Type: $STRING \times INTEGER \rightarrow INTEGER$. Type: $STRING \times INTEGER \rightarrow INTEGER$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT("1024",0) DEC_STRING_TO_INT("1024",0)
``` ```
%% Output %% Output
1024 1024
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT("1024",2) DEC_STRING_TO_INT("1024",2)
``` ```
%% Output %% Output
102400 102400
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT("1024",-1) DEC_STRING_TO_INT("1024",-1)
``` ```
%% Output %% Output
102 102
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT("1025",-1) DEC_STRING_TO_INT("1025",-1)
``` ```
%% Output %% Output
103 103
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT(" -1025",-1) DEC_STRING_TO_INT(" -1025",-1)
``` ```
%% Output %% Output
−103 −103
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT("1024.234",2) DEC_STRING_TO_INT("1024.234",2)
``` ```
%% Output %% Output
102423 102423
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT("1024",100) DEC_STRING_TO_INT("1024",100)
``` ```
%% Output %% Output
10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
DEC_STRING_TO_INT("10000000000000000000000000000000000",-32)=100 DEC_STRING_TO_INT("10000000000000000000000000000000000",-32)=100
``` ```
%% Output %% Output
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### INT_TO_DEC_STRING ### INT_TO_DEC_STRING
This external function converts an integer to a decimal string representation This external function converts an integer to a decimal string representation
with the precision provided by the second argument. with the precision provided by the second argument.
Type: $INTEGER \times INTEGER \rightarrow STRING $. Type: $INTEGER \times INTEGER \rightarrow STRING $.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_DEC_STRING(1204,2) INT_TO_DEC_STRING(1204,2)
``` ```
%% Output %% Output
"12.04" "12.04"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_DEC_STRING(-1204,3) INT_TO_DEC_STRING(-1204,3)
``` ```
%% Output %% Output
"-1.204" "-1.204"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_DEC_STRING(0,2) INT_TO_DEC_STRING(0,2)
``` ```
%% Output %% Output
"0.00" "0.00"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_DEC_STRING(1204,-2) INT_TO_DEC_STRING(1204,-2)
``` ```
%% Output %% Output
"120400" "120400"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
INT_TO_DEC_STRING(-10,3) INT_TO_DEC_STRING(-10,3)
``` ```
%% Output %% Output
"-0.010" "-0.010"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### TO_STRING ### TO_STRING
This external function converts a B data value to a string representation. This external function converts a B data value to a string representation.
Type: $\tau \rightarrow STRING$. Type: $\tau \rightarrow STRING$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
TO_STRING(1024) TO_STRING(1024)
``` ```
%% Output %% Output
"1024" "1024"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
TO_STRING("1024") TO_STRING("1024")
``` ```
%% Output %% Output
"1024" "1024"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
TO_STRING({2,3,5}) TO_STRING({2,3,5})
``` ```
%% Output %% Output
"{2,3,5}" "{2,3,5}"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
TO_STRING((TRUE,3,{11|->rec(a:22,b:33)})) TO_STRING((TRUE,3,{11|->rec(a:22,b:33)}))
``` ```
%% Output %% Output
"((TRUE|->3)|->{(11|->rec(a:22,b:33))})" "((TRUE|->3)|->{(11|->rec(a:22,b:33))})"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### FORMAT_TO_STRING ### FORMAT_TO_STRING
This external function 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. This external function 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 \verb+~w+ in the format string. - the length of sequence must correspond to the number of `~w` in the format string.
- the format string follows the conventions of SICStus Prolog. - the format string follows the conventions of SICStus Prolog.
E.g., one can use \verb+~n+ for newlines. E.g., one can use `~n` for newlines.
Type: $(STRING*seq(\tau)) \rightarrow STRING$. Type: $(STRING*seq(\tau)) \rightarrow STRING$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
FORMAT_TO_STRING("two to the power ten = ~w",[2**10]) FORMAT_TO_STRING("two to the power ten = ~w",[2**10])
``` ```
%% Output %% Output
"two to the power ten = 1024" "two to the power ten = 1024"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
FORMAT_TO_STRING("My two sets are ~w and ~w",[1..2,2..1]) FORMAT_TO_STRING("My two sets are ~w and ~w",[1..2,2..1])
``` ```
%% Output %% Output
"My two sets are {1,2} and {}" "My two sets are {1,2} and {}"
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
#### Format Strings #### Format Strings
Various external functions and predicates work with format strings. Various external functions and predicates work with format strings.
ProB uses the conventions of the SICStus Prolog format string. ProB uses the conventions of the SICStus Prolog format string.
- `~n` inserts a newline into the generated output - `~n` inserts a newline into the generated output
- `~Nn` where N is a number: it inserts $N$ newlines into the output - `~Nn` where N is a number: it inserts $N$ newlines into the output
- `~w` inserts the next argument into the generated output - `~w` inserts the next argument into the generated output
- `~i` consumes the next argument but ignores it; i.e., nothing is inserted into the output - `~i` consumes the next argument but ignores it; i.e., nothing is inserted into the output
- `~~` inserts the tilde symbol into the generated output - `~~` inserts the tilde symbol into the generated output
- `~N` inserts a newline if not at the beginning of the line - `~N` inserts a newline if not at the beginning of the line
SICStus Prolog also uses a few other formatting codes, such as `~@`, `~p`,... which should not be used. SICStus Prolog also uses a few other formatting codes, such as `~@`, `~p`,... which should not be used.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Choose Operator ## Choose Operator
You can obtain access to the definitions below by putting the following into your DEFINITIONS clause: You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "Choose.def"` `DEFINITIONS "Choose.def"`
### Choose ### Choose
This external function takes a set and returns an element of the set. This external function takes a set and returns an element of the set.
This is a proper mathematical function, i.e., it will always return the same value This is a proper mathematical function, i.e., it will always return the same value
given the same argument. given the same argument.
It is also known as Hilbert's operator. It is also known as Hilbert's operator.
The operator raises an error when it is called with an empty set. The operator raises an error when it is called with an empty set.
Also, it is not guaranteed to work for infinite sets. Also, it is not guaranteed to work for infinite sets.
Type: $POW(T) \rightarrow T$. Type: $POW(T) \rightarrow T$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Jupyter_CHOOSE MACHINE Jupyter_CHOOSE
DEFINITIONS DEFINITIONS
CHOOSE(XXX) == "a member of XXX"; CHOOSE(XXX) == "a member of XXX";
EXTERNAL_FUNCTION_CHOOSE(CHOOSE_TYPE) == (POW(CHOOSE_TYPE)-->CHOOSE_TYPE) EXTERNAL_FUNCTION_CHOOSE(CHOOSE_TYPE) == (POW(CHOOSE_TYPE)-->CHOOSE_TYPE)
END END
``` ```
%% Output %% Output
[2018-05-11 14:32:16,550, T+4478378] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh [2018-05-11 14:32:16,550, T+4478378] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-11 14:32:17,803, T+4479631] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51046 [2018-05-11 14:32:17,803, T+4479631] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51046
[2018-05-11 14:32:17,804, T+4479632] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 42415 [2018-05-11 14:32:17,804, T+4479632] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 42415
[2018-05-11 14:32:17,838, T+4479666] "ProB Output Logger for instance 4ef86d47" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop -- [2018-05-11 14:32:17,838, T+4479666] "ProB Output Logger for instance 4ef86d47" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-11 14:32:17,839, T+4479667] "ProB Output Logger for instance 4ef86d47" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1 [2018-05-11 14:32:17,839, T+4479667] "ProB Output Logger for instance 4ef86d47" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-11 14:32:17,943, T+4479771] "ProB Output Logger for instance 4ef86d47" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter_CHOOSE,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/tests]) [2018-05-11 14:32:17,943, T+4479771] "ProB Output Logger for instance 4ef86d47" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter_CHOOSE,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/tests])
Loaded machine: Jupyter_CHOOSE : [] Loaded machine: Jupyter_CHOOSE : []
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
CHOOSE(1..3) CHOOSE(1..3)
``` ```
%% Output %% Output
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
CHOOSE({1,2,3}) CHOOSE({1,2,3})
``` ```
%% Output %% Output
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
CHOOSE({"a","b","c"}) CHOOSE({"a","b","c"})
``` ```
%% Output %% Output
"a" "a"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
CHOOSE(NATURAL) CHOOSE(NATURAL)
``` ```
%% Output %% Output
0 0
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
CHOOSE(INTEGER) CHOOSE(INTEGER)
``` ```
%% Output %% Output
0 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The operator is useful for writing WHILE loops or recursive functions which manipulate sets. The operator is useful for writing WHILE loops or recursive functions which manipulate sets.
The following example defines a recursive summation function using the CHOOSE operator. The following example defines a recursive summation function using the CHOOSE operator.
` `
MACHINE RecursiveSigmaCHOOSEv3 MACHINE RecursiveSigmaCHOOSEv3
DEFINITIONS DEFINITIONS
"Choose.def" "Choose.def"
ABSTRACT_CONSTANTS sigma ABSTRACT_CONSTANTS sigma
PROPERTIES PROPERTIES
sigma: POW(INTEGER) <-> INTEGER & sigma: POW(INTEGER) <-> INTEGER &
sigma = %x.(x:POW(INTEGER) | sigma = %x.(x:POW(INTEGER) |
IF x={} THEN 0 ELSE IF x={} THEN 0 ELSE
LET c BE c=CHOOSE(x) IN c+sigma(x-{c}) END LET c BE c=CHOOSE(x) IN c+sigma(x-{c}) END
END END
) )
ASSERTIONS ASSERTIONS
sigma({3,5,7}) = 15; sigma({3,5,7}) = 15;
END END
` `
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment