From d8a072adae34fce6dcfc8f5f37acdba52dd2e339 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Fri, 11 May 2018 13:35:38 +0200
Subject: [PATCH] add first version of manual

---
 notebooks/manual/ExternalFunctions.ipynb | 539 +++++++++++++++++++++++
 1 file changed, 539 insertions(+)
 create mode 100644 notebooks/manual/ExternalFunctions.ipynb

diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb
new file mode 100644
index 0000000..8649e0d
--- /dev/null
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -0,0 +1,539 @@
+{
+ "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
+}
-- 
GitLab