add first version of manual

d8a072ad · Michael Leuschel · 04f87a4e · d8a072ad
Commit d8a072ad authored May 11, 2018 by Michael Leuschel
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# External Functions\n",
+    "## LibraryStrings\n",
+    "\n",
+    "In pure B there are only two built-in operators on strings: equality $=$ and inequality $\\neq$.\n",
+    "This library provides several string manipulation functions, and assumes that STRINGS are\n",
+    " sequences of unicode characters (in UTF-8 encoding).\n",
+    "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+    "\n",
+    "`DEFINITIONS \"LibraryStrings.def\"`\n",
+    "\n",
+    "The file `LibraryStrings.def` is bundled with ProB and can be found in the `stdlib` folder.\n",
+    "You can also include the machine `LibraryStrings.mch` instead of the definition file;\n",
+    " the machine defines some of the functions below as proper B functions (i.e., functions\n",
+    " for which you can compute the domain and use constructs such as\n",
+    " relational image)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "[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\n",
+      "[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\n",
+      "[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\n",
+      "[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 --\u001b[0m\n",
+      "[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\u001b[0m\n",
+      "[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])\u001b[0m\n"
+     ]
+    },
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Jupyter : []\n"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Jupyter\n",
+    "DEFINITIONS  // \"LibraryStrings.def\"\n",
+    "  STRING_LENGTH(xxx) == length(xxx);\n",
+    "  EXTERNAL_FUNCTION_STRING_LENGTH == STRING --> INTEGER;\n",
+    "  \n",
+    "  /* This external function takes two strings and concatenates them. */\n",
+    "  STRING_APPEND(xxx,yyy) == append(xxx,yyy);\n",
+    "  EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;\n",
+    "\n",
+    "  /* This external function takes a sequence of strings and concatenates them. */\n",
+    "  STRING_CONC(string_conc_list) == \"\";\n",
+    "  EXTERNAL_FUNCTION_STRING_CONC == seq(STRING) --> STRING;\n",
+    "  \n",
+    "  /* This external function takes two strings and separates the first string\n",
+    "     according to the separator specified by the second string. */\n",
+    "  STRING_SPLIT(xxx,yyy) == split(xxx,yyy);\n",
+    "  EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));\n",
+    "  \n",
+    "  /* This external function takes a sequence of strings and a separator string\n",
+    "     and joins the strings together inserting the separators as often as needed.\n",
+    "     It is the inverse of the STRING_SPLIT function. */\n",
+    "  STRING_JOIN(xxx,yyy) == join(xxx,yyy);\n",
+    "  EXTERNAL_FUNCTION_STRING_JOIN == (((INTEGER<->STRING)*STRING) --> STRING);\n",
+    "  \n",
+    "  STRING_CHARS(xxx) == chars(xxx);\n",
+    "  EXTERNAL_FUNCTION_STRING_CHARS == (STRING --> (INTEGER<->STRING));\n",
+    "  \n",
+    "  STRING_CODES(xxx) == codes(xxx);\n",
+    "  EXTERNAL_FUNCTION_STRING_CODES == (STRING --> (INTEGER<->INTEGER));\n",
+    "  \n",
+    "  /* This external function takes a string and converts it into an integer.\n",
+    "     An error is raised if this cannot be done.\n",
+    "     It is safer to first check with {\\tt STRING\\_IS\\_INT} whether the conversion can be done. */\n",
+    "  STRING_TO_INT(sss) == 0;\n",
+    "  EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER);\n",
+    "  \n",
+    "  /* This external predicate takes a string and is true if the string represents an integer. */\n",
+    "  STRING_IS_INT(sss) == (1=1);\n",
+    "  EXTERNAL_PREDICATE_STRING_IS_INT == (STRING);\n",
+    "  \n",
+    "  /* This external function takes a decimal string (with optional decimal places)\n",
+    "      and converts it to an integer with the given precision. */\n",
+    "  EXTERNAL_FUNCTION_DEC_STRING_TO_INT == STRING * INTEGER --> INTEGER;\n",
+    "  DEC_STRING_TO_INT(decimal_string,precision) == 0;\n",
+    "  \n",
+    "   /* parametric function; cannot be represented as constant function : */\n",
+    "  STRING_TO_ENUM(sss) ==({}(1)); /* Note: you have to include the DEFINITION into your B file */\n",
+    "  EXTERNAL_FUNCTION_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == (STRING --> STRING_TO_ENUM_TYPE);\n",
+    "  TYPED_STRING_TO_ENUM(t,sss) ==({}(1));\n",
+    "  EXTERNAL_FUNCTION_TYPED_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == \n",
+    "                      (POW(STRING_TO_ENUM_TYPE)*STRING --> STRING_TO_ENUM_TYPE);\n",
+    "  \n",
+    "  /* This external function converts an integer to a string representation. */\n",
+    "  INT_TO_STRING(sss) == \"0\";\n",
+    "  EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING);\n",
+    "  \n",
+    "  /* This external function converts an integer to a decimal string representation\n",
+    "     with the precision provided by the second argument. */\n",
+    "  INT_TO_DEC_STRING(integer,precision) == \"0.0\";\n",
+    "  EXTERNAL_FUNCTION_INT_TO_DEC_STRING == (INTEGER*INTEGER --> STRING);\n",
+    "  \n",
+    "  /* This external function converts a B data value to a string representation. */\n",
+    "  TO_STRING(sss) == \"0\";\n",
+    "  EXTERNAL_FUNCTION_TO_STRING(TO_STRING_TYPE) == (TO_STRING_TYPE --> STRING);\n",
+    "  \n",
+    "  /* This external function takes a format string and a B sequence of values and generates an output\n",
+    "     string, where the values have been inserted into the format string in place of the ~w placeholders.\n",
+    "   */\n",
+    "  FORMAT_TO_STRING(MyFormatString,ListOfValues) == \"0\";\n",
+    "  EXTERNAL_FUNCTION_FORMAT_TO_STRING(FORMAT_TO_STRING_TYPE) == ((STRING*seq(FORMAT_TO_STRING_TYPE)) --> STRING);\n",
+    "  \n",
+    "  /* This external function checks whether the second string occurs contiguously within the first string. */\n",
+    "  EXTERNAL_FUNCTION_STRING_CONTAINS_STRING == (STRING*STRING)--> BOOL;\n",
+    "  STRING_CONTAINS_STRING(arg1,arg2)==FALSE; // TRUE when arg2 occurs as contiguous substring in arg1\n",
+    "\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### STRING_APPEND\n",
+    "\n",
+    "This external function takes two strings and concatenates them.\n",
+    "\n",
+    "Type: $STRING \\times STRING \\rightarrow STRING $."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\"abcabc\""
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_APPEND(\"abc\",\"abc\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\"abc\""
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_APPEND(\"abc\",\"\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### STRING_LENGTH\n",
+    "\n",
+    "This external function takes a string and returns the length.\n",
+    "\n",
+    "Type: $STRING \\rightarrow INTEGER$."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "3"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_LENGTH(\"abc\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "0"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_LENGTH(\"\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### STRING_SPLIT\n",
+    "\n",
+    "This external function takes two strings and separates the first string\n",
+    " according to the separator specified by the second string.\n",
+    "\n",
+    "Type: $STRING \\times STRING \\rightarrow \\mathit{seq}(STRING) $."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "{(1↦\"filename\"),(2↦\"ext\")}"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_SPLIT(\"filename.ext\",\".\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "{(1↦\"filename.ext\")}"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_SPLIT(\"filename.ext\",\"/\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "[\"usr\",\"local\",\"lib\"]"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_SPLIT(\"usr/local/lib\",\"/\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "{(1↦\"\")}"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_SPLIT(\"\",\".\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "I am not sure the following result makes sense, maybe a sequence of all characters is more appropriate?"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "{(1↦\"usr/local/lib\")}"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_SPLIT(\"usr/local/lib\",\"\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "{(1↦\"usr/lo\"),(2↦\"/lib\")}"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_SPLIT(\"usr/local/lib\",\"cal\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### STRING_JOIN\n",
+    "This external function takes a sequence of strings and a separator string\n",
+    " and joins the strings together inserting the separators as often as needed.\n",
+    "It is the inverse of the `STRING_SPLIT` function.\n",
+    "\n",
+    "Type: $\\mathit{seq}(STRING) \\times STRING \\rightarrow STRING $."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\"usr/local/lib\""
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_JOIN([\"usr\",\"local\",\"lib\"],\"/\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\"usr/local/lib\""
+      ]
+     },
+     "execution_count": 15,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_JOIN([\"usr/lo\",\"/lib\"],\"cal\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\"usr/local/lib\""
+      ]
+     },
+     "execution_count": 16,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_JOIN([\"usr/local/lib\"],\"\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### STRING_CHARS\n",
+    "\n",
+    "This external function takes a strings splits it into a sequence\n",
+    "of the individual characters. Each character is represented by a string.\n",
+    "\n",
+    "Type: $STRING \\rightarrow \\mathit{seq}(STRING) $."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "∅"
+      ]
+     },
+     "execution_count": 17,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_CHARS(\"\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "[\"a\",\"b\",\"c\"]"
+      ]
+     },
+     "execution_count": 18,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_CHARS(\"abc\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 19,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\"a.b.c\""
+      ]
+     },
+     "execution_count": 19,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_JOIN(STRING_CHARS(\"abc\"),\".\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "ProB 2",
+   "language": "prob",
+   "name": "prob2"
+  },
+  "language_info": {
+   "file_extension": ".prob",
+   "mimetype": "text/x-prob",
+   "name": "prob"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
+%% Cell type:markdown id: tags:
+
+# External Functions
+## LibraryStrings
+
+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
+ sequences of unicode characters (in UTF-8 encoding).
+You can obtain the definitions below 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).
+
+%% Cell type:code id: tags:
+
+``` prob
+::load
+MACHINE Jupyter
+DEFINITIONS  // "LibraryStrings.def"
+  STRING_LENGTH(xxx) == length(xxx);
+  EXTERNAL_FUNCTION_STRING_LENGTH == STRING --> INTEGER;
+
+  /* This external function takes two strings and concatenates them. */
+  STRING_APPEND(xxx,yyy) == append(xxx,yyy);
+  EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;
+
+  /* This external function takes a sequence of strings and concatenates them. */
+  STRING_CONC(string_conc_list) == "";
+  EXTERNAL_FUNCTION_STRING_CONC == seq(STRING) --> STRING;
+
+  /* This external function takes two strings and separates the first string
+     according to the separator specified by the second string. */
+  STRING_SPLIT(xxx,yyy) == split(xxx,yyy);
+  EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->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.
+     It is the inverse of the STRING_SPLIT function. */
+  STRING_JOIN(xxx,yyy) == join(xxx,yyy);
+  EXTERNAL_FUNCTION_STRING_JOIN == (((INTEGER<->STRING)*STRING) --> STRING);
+
+  STRING_CHARS(xxx) == chars(xxx);
+  EXTERNAL_FUNCTION_STRING_CHARS == (STRING --> (INTEGER<->STRING));
+
+  STRING_CODES(xxx) == codes(xxx);
+  EXTERNAL_FUNCTION_STRING_CODES == (STRING --> (INTEGER<->INTEGER));
+
+  /* This external function 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 {\tt STRING\_IS\_INT} whether the conversion can be done. */
+  STRING_TO_INT(sss) == 0;
+  EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER);
+
+  /* This external predicate takes a string and is true if the string represents an integer. */
+  STRING_IS_INT(sss) == (1=1);
+  EXTERNAL_PREDICATE_STRING_IS_INT == (STRING);
+
+  /* This external function takes a decimal string (with optional decimal places)
+      and converts it to an integer with the given precision. */
+  EXTERNAL_FUNCTION_DEC_STRING_TO_INT == STRING * INTEGER --> INTEGER;
+  DEC_STRING_TO_INT(decimal_string,precision) == 0;
+
+   /* parametric function; cannot be represented as constant function : */
+  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);
+  TYPED_STRING_TO_ENUM(t,sss) ==({}(1));
+  EXTERNAL_FUNCTION_TYPED_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) ==
+                      (POW(STRING_TO_ENUM_TYPE)*STRING --> STRING_TO_ENUM_TYPE);
+
+  /* This external function converts an integer to a string representation. */
+  INT_TO_STRING(sss) == "0";
+  EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING);
+
+  /* This external function converts an integer to a decimal string representation
+     with the precision provided by the second argument. */
+  INT_TO_DEC_STRING(integer,precision) == "0.0";
+  EXTERNAL_FUNCTION_INT_TO_DEC_STRING == (INTEGER*INTEGER --> STRING);
+
+  /* This external function converts a B data value to a string representation. */
+  TO_STRING(sss) == "0";
+  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
+     string, where the values have been inserted into the format string in place of the ~w placeholders.
+   */
+  FORMAT_TO_STRING(MyFormatString,ListOfValues) == "0";
+  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. */
+  EXTERNAL_FUNCTION_STRING_CONTAINS_STRING == (STRING*STRING)--> BOOL;
+  STRING_CONTAINS_STRING(arg1,arg2)==FALSE; // TRUE when arg2 occurs as contiguous substring in arg1
+
+END
+```
+
+%% 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: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,904, T+247732] "ProB Output Logger for instance 342c2add" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --[0m
+    [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[0m
+    [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])[0m
+
+    Loaded machine: Jupyter : []
+
+%% Cell type:markdown id: tags:
+
+### STRING_APPEND
+
+This external function takes two strings and concatenates them.
+
+Type: $STRING \times STRING \rightarrow STRING $.
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_APPEND("abc","abc")
+```
+
+%% Output
+
+    "abcabc"
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_APPEND("abc","")
+```
+
+%% Output
+
+    "abc"
+
+%% Cell type:markdown id: tags:
+
+### STRING_LENGTH
+
+This external function takes a string and returns the length.
+
+Type: $STRING \rightarrow INTEGER$.
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_LENGTH("abc")
+```
+
+%% Output
+
+    3
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_LENGTH("")
+```
+
+%% Output
+
+    0
+
+%% Cell type:markdown id: tags:
+
+### STRING_SPLIT
+
+This external function takes two strings and separates the first string
+ according to the separator specified by the second string.
+
+Type: $STRING \times STRING \rightarrow \mathit{seq}(STRING) $.
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_SPLIT("filename.ext",".")
+```
+
+%% Output
+
+    {(1↦"filename"),(2↦"ext")}
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_SPLIT("filename.ext","/")
+```
+
+%% Output
+
+    {(1↦"filename.ext")}
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_SPLIT("usr/local/lib","/")
+```
+
+%% Output
+
+    ["usr","local","lib"]
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_SPLIT("",".")
+```
+
+%% Output
+
+    {(1↦"")}
+
+%% Cell type:markdown id: tags:
+
+I am not sure the following result makes sense, maybe a sequence of all characters is more appropriate?
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_SPLIT("usr/local/lib","")
+```
+
+%% Output
+
+    {(1↦"usr/local/lib")}
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_SPLIT("usr/local/lib","cal")
+```
+
+%% Output
+
+    {(1↦"usr/lo"),(2↦"/lib")}
+
+%% Cell type:markdown id: tags:
+
+### STRING_JOIN
+This external function 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.
+
+Type: $\mathit{seq}(STRING) \times STRING \rightarrow STRING $.
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_JOIN(["usr","local","lib"],"/")
+```
+
+%% Output
+
+    "usr/local/lib"
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_JOIN(["usr/lo","/lib"],"cal")
+```
+
+%% Output
+
+    "usr/local/lib"
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_JOIN(["usr/local/lib"],"")
+```
+
+%% Output
+
+    "usr/local/lib"
+
+%% Cell type:markdown id: tags:
+
+### STRING_CHARS
+
+This external function takes a strings splits it into a sequence
+of the individual characters. Each character is represented by a string.
+
+Type: $STRING \rightarrow \mathit{seq}(STRING) $.
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_CHARS("")
+```
+
+%% Output
+
+    ∅
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_CHARS("abc")
+```
+
+%% Output
+
+    ["a","b","c"]
+
+%% Cell type:code id: tags:
+
+``` prob
+STRING_JOIN(STRING_CHARS("abc"),".")
+```
+
+%% Output
+
+    "a.b.c"
+
+%% Cell type:code id: tags:
+
+``` prob
+```