{ "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": 1, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[2018-05-13 09:48:02,007, T+3926] \"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-13 09:48:03,239, T+5158] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54031\n", "[2018-05-13 09:48:03,240, T+5159] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62735\n", "[2018-05-13 09:48:03,243, T+5162] \"ProB Output Logger for instance 4f9c1863\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", "[2018-05-13 09:48:03,263, T+5182] \"ProB Output Logger for instance 4f9c1863\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", "[2018-05-13 09:48:03,386, T+5305] \"ProB Output Logger for instance 4f9c1863\" 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/manual])\u001b[0m\n" ] }, { "data": { "text/plain": [ "Loaded machine: Jupyter : []\n" ] }, "execution_count": 1, "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": 2, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"abcabc\"" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_APPEND(\"abc\",\"abc\")" ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"abc\"" ] }, "execution_count": 3, "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": 4, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "3" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_LENGTH(\"abc\")" ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 5, "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": 6, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "{(1↦\"filename\"),(2↦\"ext\")}" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_SPLIT(\"filename.ext\",\".\")" ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "{(1↦\"filename.ext\")}" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_SPLIT(\"filename.ext\",\"/\")" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[\"usr\",\"local\",\"lib\"]" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_SPLIT(\"usr/local/lib\",\"/\")" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "{(1↦\"\")}" ] }, "execution_count": 9, "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": 10, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "{(1↦\"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↦\"usr/lo\"),(2↦\"/lib\")}" ] }, "execution_count": 11, "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": 12, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"usr/local/lib\"" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_JOIN([\"usr\",\"local\",\"lib\"],\"/\")" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"usr/local/lib\"" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_JOIN([\"usr/lo\",\"/lib\"],\"cal\")" ] }, { "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": "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": 15, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_CHARS(\"\")" ] }, { "cell_type": "code", "execution_count": 16, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[\"a\",\"b\",\"c\"]" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_CHARS(\"abc\")" ] }, { "cell_type": "code", "execution_count": 17, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"a.b.c\"" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_JOIN(STRING_CHARS(\"abc\"),\".\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### STRING_CODES\n", "\n", "This external function takes a strings splits it into a sequence\n", "of the individual characters. Each character is represented by a natural number\n", " (the ASCII or Unicode representation of the character).\n", "\n", "Type: $STRING \\rightarrow \\mathit{seq}(INTEGER) $." ] }, { "cell_type": "code", "execution_count": 18, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_CODES(\"\")" ] }, { "cell_type": "code", "execution_count": 19, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[65,90,32,97,122,32,48,57]" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_CODES(\"AZ az 09\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### STRING_IS_INT" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "\n", "This external predicate takes a string and is true if the string represents an integer.\n", "\n", "Type: $STRING $." ] }, { "cell_type": "code", "execution_count": 20, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"1204\")" ] }, { "cell_type": "code", "execution_count": 21, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 21, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"-1204\")" ] }, { "cell_type": "code", "execution_count": 22, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\" - 1204\")" ] }, { "cell_type": "code", "execution_count": 23, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "FALSE" ] }, "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"1.1\")" ] }, { "cell_type": "code", "execution_count": 24, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "FALSE" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"1.0\")" ] }, { "cell_type": "code", "execution_count": 25, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "FALSE" ] }, "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"a\")" ] }, { "cell_type": "code", "execution_count": 26, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 26, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"1000000000000000000000000000\")" ] }, { "cell_type": "code", "execution_count": 27, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"-00001\")" ] }, { "cell_type": "code", "execution_count": 28, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 28, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_IS_INT(\"00002\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### STRING_TO_INT\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 `STRING_IS_INT` whether the conversion can be done.\n", "\n", "Type: $STRING \\rightarrow INTEGER$." ] }, { "cell_type": "code", "execution_count": 29, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1024" ] }, "execution_count": 29, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_TO_INT(\"1024\")" ] }, { "cell_type": "code", "execution_count": 30, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "−1" ] }, "execution_count": 30, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_TO_INT(\" - 00001\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### INT_TO_STRING\n", "\n", "This external function converts an integer to a string representation.\n", "\n", "Type: $INTEGER \\rightarrow STRING $." ] }, { "cell_type": "code", "execution_count": 31, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"1024\"" ] }, "execution_count": 31, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_STRING(1024)" ] }, { "cell_type": "code", "execution_count": 32, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"-1024\"" ] }, "execution_count": 32, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_STRING(-1024)" ] }, { "cell_type": "code", "execution_count": 33, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"-1\"" ] }, "execution_count": 33, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_STRING(STRING_TO_INT(\" - 00001\"))" ] }, { "cell_type": "code", "execution_count": 34, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 34, "metadata": {}, "output_type": "execute_result" } ], "source": [ "STRING_TO_INT(INT_TO_STRING(-1))=-1" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### DEC_STRING_TO_INT\n", "\n", "This external function takes a decimal string (with optional decimal places) and converts it to an integer with the given precision (rounding if required).\n", "\n", "Type: $STRING \\times INTEGER \\rightarrow INTEGER$." ] }, { "cell_type": "code", "execution_count": 35, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1024" ] }, "execution_count": 35, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\"1024\",0)" ] }, { "cell_type": "code", "execution_count": 36, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "102400" ] }, "execution_count": 36, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\"1024\",2)" ] }, { "cell_type": "code", "execution_count": 37, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "102" ] }, "execution_count": 37, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\"1024\",-1)" ] }, { "cell_type": "code", "execution_count": 38, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "103" ] }, "execution_count": 38, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\"1025\",-1)" ] }, { "cell_type": "code", "execution_count": 39, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "−103" ] }, "execution_count": 39, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\" -1025\",-1)" ] }, { "cell_type": "code", "execution_count": 40, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "102423" ] }, "execution_count": 40, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\"1024.234\",2)" ] }, { "cell_type": "code", "execution_count": 41, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" ] }, "execution_count": 41, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\"1024\",100)" ] }, { "cell_type": "code", "execution_count": 42, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "TRUE" ] }, "execution_count": 42, "metadata": {}, "output_type": "execute_result" } ], "source": [ "DEC_STRING_TO_INT(\"10000000000000000000000000000000000\",-32)=100" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### INT_TO_DEC_STRING\n", "\n", "This external function converts an integer to a decimal string representation\n", " with the precision provided by the second argument.\n", "\n", "Type: $INTEGER \\times INTEGER \\rightarrow STRING $." ] }, { "cell_type": "code", "execution_count": 43, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"12.04\"" ] }, "execution_count": 43, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_DEC_STRING(1204,2)" ] }, { "cell_type": "code", "execution_count": 44, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"-1.204\"" ] }, "execution_count": 44, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_DEC_STRING(-1204,3)" ] }, { "cell_type": "code", "execution_count": 45, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"0.00\"" ] }, "execution_count": 45, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_DEC_STRING(0,2)" ] }, { "cell_type": "code", "execution_count": 46, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"120400\"" ] }, "execution_count": 46, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_DEC_STRING(1204,-2)" ] }, { "cell_type": "code", "execution_count": 47, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"-0.010\"" ] }, "execution_count": 47, "metadata": {}, "output_type": "execute_result" } ], "source": [ "INT_TO_DEC_STRING(-10,3)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### TO_STRING\n", "\n", "This external function converts a B data value to a string representation.\n", "\n", "Type: $\\tau \\rightarrow STRING$." ] }, { "cell_type": "code", "execution_count": 48, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"1024\"" ] }, "execution_count": 48, "metadata": {}, "output_type": "execute_result" } ], "source": [ "TO_STRING(1024)" ] }, { "cell_type": "code", "execution_count": 49, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"1024\"" ] }, "execution_count": 49, "metadata": {}, "output_type": "execute_result" } ], "source": [ "TO_STRING(\"1024\")" ] }, { "cell_type": "code", "execution_count": 50, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"{2,3,5}\"" ] }, "execution_count": 50, "metadata": {}, "output_type": "execute_result" } ], "source": [ "TO_STRING({2,3,5})" ] }, { "cell_type": "code", "execution_count": 51, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"((TRUE|->3)|->{(11|->rec(a:22,b:33))})\"" ] }, "execution_count": 51, "metadata": {}, "output_type": "execute_result" } ], "source": [ "TO_STRING((TRUE,3,{11|->rec(a:22,b:33)}))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### FORMAT_TO_STRING\n", "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.\n", " - the length of sequence must correspond to the number of `~w` in the format string.\n", " - the format string follows the conventions of SICStus Prolog.\n", " E.g., one can use `~n` for newlines.\n", "\n", "\n", "Type: $(STRING*seq(\\tau)) \\rightarrow STRING$." ] }, { "cell_type": "code", "execution_count": 52, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"two to the power ten = 1024\"" ] }, "execution_count": 52, "metadata": {}, "output_type": "execute_result" } ], "source": [ "FORMAT_TO_STRING(\"two to the power ten = ~w\",[2**10])" ] }, { "cell_type": "code", "execution_count": 53, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"My two sets are {1,2} and {}\"" ] }, "execution_count": 53, "metadata": {}, "output_type": "execute_result" } ], "source": [ "FORMAT_TO_STRING(\"My two sets are ~w and ~w\",[1..2,2..1])" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### Format Strings\n", "\n", "Various external functions and predicates work with format strings.\n", "ProB uses the conventions of the SICStus Prolog format string.\n", " - `~n` inserts a newline into the generated output\n", " - `~Nn` where N is a number: it inserts $N$ newlines into the output\n", " - `~w` inserts the next argument into the generated output\n", " - `~i` consumes the next argument but ignores it; i.e., nothing is inserted into the output\n", " - `~~` inserts the tilde symbol into the generated output\n", " - `~N` inserts a newline if not at the beginning of the line\n", "\n", "SICStus Prolog also uses a few other formatting codes, such as `~@`, `~p`,... which should not be used." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Choose Operator\n", "You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n", " `DEFINITIONS \"Choose.def\"`\n", "\n", "### Choose\n", "\n", "This external function takes a set and returns an element of the set.\n", "This is a proper mathematical function, i.e., it will always return the same value\n", "given the same argument.\n", "It is also known as Hilbert's operator.\n", "\n", "The operator raises an error when it is called with an empty set.\n", "Also, it is not guaranteed to work for infinite sets.\n", "\n", "Type: $POW(T) \\rightarrow T$." ] }, { "cell_type": "code", "execution_count": 54, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[2018-05-13 09:48:06,965, T+8884] \"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-13 09:48:08,087, T+10006] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54038\n", "[2018-05-13 09:48:08,088, T+10007] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62740\n", "[2018-05-13 09:48:08,090, T+10009] \"ProB Output Logger for instance 2f1db1bc\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", "[2018-05-13 09:48:08,107, T+10026] \"ProB Output Logger for instance 2f1db1bc\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", "[2018-05-13 09:48:08,207, T+10126] \"ProB Output Logger for instance 2f1db1bc\" 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/manual])\u001b[0m\n" ] }, { "data": { "text/plain": [ "Loaded machine: Jupyter_CHOOSE : []\n" ] }, "execution_count": 54, "metadata": {}, "output_type": "execute_result" } ], "source": [ "::load\n", "MACHINE Jupyter_CHOOSE\n", "DEFINITIONS\n", " CHOOSE(XXX) == \"a member of XXX\";\n", " EXTERNAL_FUNCTION_CHOOSE(CHOOSE_TYPE) == (POW(CHOOSE_TYPE)-->CHOOSE_TYPE)\n", " END" ] }, { "cell_type": "code", "execution_count": 55, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1" ] }, "execution_count": 55, "metadata": {}, "output_type": "execute_result" } ], "source": [ "CHOOSE(1..3)" ] }, { "cell_type": "code", "execution_count": 56, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1" ] }, "execution_count": 56, "metadata": {}, "output_type": "execute_result" } ], "source": [ "CHOOSE({1,2,3})" ] }, { "cell_type": "code", "execution_count": 57, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"a\"" ] }, "execution_count": 57, "metadata": {}, "output_type": "execute_result" } ], "source": [ "CHOOSE({\"a\",\"b\",\"c\"})" ] }, { "cell_type": "code", "execution_count": 58, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 58, "metadata": {}, "output_type": "execute_result" } ], "source": [ "CHOOSE(NATURAL)" ] }, { "cell_type": "code", "execution_count": 59, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 59, "metadata": {}, "output_type": "execute_result" } ], "source": [ "CHOOSE(INTEGER)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The operator is useful for writing WHILE loops or recursive functions which manipulate sets.\n", "The following example defines a recursive summation function using the CHOOSE operator.\n", "\n", "`\n", "MACHINE RecursiveSigmaCHOOSEv3\n", "DEFINITIONS\n", " \"Choose.def\"\n", "ABSTRACT_CONSTANTS sigma\n", "PROPERTIES\n", " sigma: POW(INTEGER) <-> INTEGER &\n", " sigma = %x.(x:POW(INTEGER) |\n", " IF x={} THEN 0 ELSE\n", " LET c BE c=CHOOSE(x) IN c+sigma(x-{c}) END\n", " END\n", " )\n", "ASSERTIONS\n", " sigma({3,5,7}) = 15;\n", "END\n", "`" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Sorting Sets\n", "You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n", "`DEFINITIONS \"SORT.def\"`\n", "\n", "Alternatively you can use the following if you use ProB prior to version 1.7.1:\n", "`\n", "DEFINITIONS\n", " SORT(X) == [];\n", " EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T));\n", "`\n", "\n", "This external function SORT takes a set and translates it into a B sequence.\n", "It uses ProB's internal order for sorting the elements.\n", "It will not work for infinite sets.\n", "Type: $POW(\\tau) \\rightarrow seq(\\tau)$." ] }, { "cell_type": "code", "execution_count": 60, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[2018-05-13 09:48:08,755, T+10674] \"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-13 09:48:09,935, T+11854] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54042\n", "[2018-05-13 09:48:09,935, T+11854] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62744\n", "[2018-05-13 09:48:09,937, T+11856] \"ProB Output Logger for instance f4b34d8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", "[2018-05-13 09:48:09,963, T+11882] \"ProB Output Logger for instance f4b34d8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", "[2018-05-13 09:48:10,084, T+12003] \"ProB Output Logger for instance f4b34d8\" 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/manual])\u001b[0m\n" ] }, { "data": { "text/plain": [ "Loaded machine: Jupyter_CHOOSE : []\n" ] }, "execution_count": 60, "metadata": {}, "output_type": "execute_result" } ], "source": [ "::load\n", "MACHINE Jupyter_CHOOSE\n", "DEFINITIONS\n", " SORT(X) == [];\n", " EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T))\n", " END" ] }, { "cell_type": "code", "execution_count": 61, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[1,2,3]" ] }, "execution_count": 61, "metadata": {}, "output_type": "execute_result" } ], "source": [ "SORT(1..3)" ] }, { "cell_type": "code", "execution_count": 62, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[6,9,27]" ] }, "execution_count": 62, "metadata": {}, "output_type": "execute_result" } ], "source": [ "SORT({3*3,3+3,3**3})" ] }, { "cell_type": "code", "execution_count": 63, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[\"1\",\"10\",\"11\",\"2\",\"a\",\"aa\",\"ab\",\"b\"]" ] }, "execution_count": 63, "metadata": {}, "output_type": "execute_result" } ], "source": [ "SORT({\"ab\",\"aa\",\"a\",\"b\",\"10\",\"1\",\"2\",\"11\"})" ] }, { "cell_type": "code", "execution_count": 64, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[(\"a\"↦0),(\"a\"↦1),(\"b\"↦0)]" ] }, "execution_count": 64, "metadata": {}, "output_type": "execute_result" } ], "source": [ "SORT({(\"a\"|->1),(\"b\"|->0),(\"a\"|->0)})" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "A related external function is LEQ_SYM_BREAK which allows one to compare values of arbitrary type.\n", "Calls to this external function are automatically\n", "inserted by ProB for symmetry breaking of quantifiers.\n", "It should currently not be used for sets or sequences." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## LibraryMeta\n", "This library provides various meta information about ProB and the current model.\n", "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n", "\n", "`DEFINITIONS \"LibraryMeta.def\"`\n", "\n", "The file `LibraryMeta.def` is also bundled with ProB and can be found in the `stdlib` folder." ] }, { "cell_type": "code", "execution_count": 84, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[2018-05-13 10:25:48,398, T+2270317] \"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-13 10:25:49,665, T+2271584] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 56523\n", "[2018-05-13 10:25:49,666, T+2271585] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 63566\n", "[2018-05-13 10:25:49,670, T+2271589] \"ProB Output Logger for instance 26a501d7\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", "[2018-05-13 10:25:49,687, T+2271606] \"ProB Output Logger for instance 26a501d7\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", "[2018-05-13 10:25:49,803, T+2271722] \"ProB Output Logger for instance 26a501d7\" 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/manual])\u001b[0m\n" ] }, { "data": { "text/plain": [ "Loaded machine: Jupyter : []\n" ] }, "execution_count": 84, "metadata": {}, "output_type": "execute_result" } ], "source": [ "::load\n", "MACHINE Jupyter\n", "DEFINITIONS\n", " EXTERNAL_FUNCTION_PROB_INFO_STR == STRING --> STRING;\n", " PROB_INFO_STR(info_field_name) == \"\";\n", " EXTERNAL_FUNCTION_PROB_STATISTICS == STRING --> INTEGER;\n", " PROB_STATISTICS(info_field_name) == 0;\n", " EXTERNAL_FUNCTION_PROJECT_INFO == STRING --> POW(STRING);\n", " PROJECT_INFO(info_field_name) == {};\n", " EXTERNAL_FUNCTION_PROJECT_STATISTICS == STRING --> INTEGER;\n", " PROJECT_STATISTICS(info_field_name) == 0;\n", " EXTERNAL_FUNCTION_MACHINE_INFO == STRING * STRING --> STRING;\n", " MACHINE_INFO(info_field_name,machine) == \"\"\n", "END" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### PROB_INFO_STR\n", "This external function provides access to various information strings about ProB.\n", "Type: $STRING \\rightarrow STRING$." ] }, { "cell_type": "code", "execution_count": 68, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"1.8.1-beta4\"" ] }, "execution_count": 68, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_INFO_STR(\"prob-version\")" ] }, { "cell_type": "code", "execution_count": 70, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"d30772a772f686c7972a16ddcb7fe9d79e4af54f\"" ] }, "execution_count": 70, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_INFO_STR(\"prob-revision\")" ] }, { "cell_type": "code", "execution_count": 82, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"Fri May 11 14:29:42 2018 +0200\"" ] }, "execution_count": 82, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_INFO_STR(\"prob-last-changed-date\")" ] }, { "cell_type": "code", "execution_count": 71, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"1.8.0_152-b16\"" ] }, "execution_count": 71, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_INFO_STR(\"java-version\")" ] }, { "cell_type": "code", "execution_count": 80, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"/usr/bin/java\"" ] }, "execution_count": 80, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_INFO_STR(\"java-command-path\")" ] }, { "cell_type": "code", "execution_count": 81, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "\"13/5/2018 - 10h18 8s\"" ] }, "execution_count": 81, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_INFO_STR(\"current-time\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Another command is PROB_INFO_STR(\"parser-version\") which does not work within Jupyter." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### PROB_STATISTICS\n", "This external function provides access to various statistics in the form of integers about ProB.\n", "Type: $STRING \\rightarrow INTEGER$." ] }, { "cell_type": "code", "execution_count": 73, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "150527440" ] }, "execution_count": 73, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"prolog-memory-bytes-used\")" ] }, { "cell_type": "code", "execution_count": 74, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1" ] }, "execution_count": 74, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"states\")" ] }, { "cell_type": "code", "execution_count": 75, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 75, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"transitions\")" ] }, { "cell_type": "code", "execution_count": 76, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 76, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"processed-states\")" ] }, { "cell_type": "code", "execution_count": 77, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "−1" ] }, "execution_count": 77, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"current-state-id\")" ] }, { "cell_type": "code", "execution_count": 78, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1526199415" ] }, "execution_count": 78, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"now-timestamp\")" ] }, { "cell_type": "code", "execution_count": 79, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1320" ] }, "execution_count": 79, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"prolog-runtime\")" ] }, { "cell_type": "code", "execution_count": 83, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1054870" ] }, "execution_count": 83, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROB_STATISTICS(\"prolog-walltime\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Other possible information fields are prolog-memory-bytes-free,\n", "prolog-global-stack-bytes-used,\n", "prolog-local-stack-bytes-used,\n", "prolog-global-stack-bytes-free,\n", "prolog-local-stack-bytes-free,\n", "prolog-trail-bytes-used,\n", "prolog-choice-bytes-used,\n", "prolog-atoms-bytes-used,\n", "prolog-atoms-nb-used,\n", "prolog-gc-count,\n", "prolog-gc-time." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### PROJECT_STATISTICS\n", "This external function provides access to various statistics in the form of integers about the current specification being processed, with all auxiliary files (i.e., project).\n", "Type: $STRING \\rightarrow INTEGER$." ] }, { "cell_type": "code", "execution_count": 86, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 86, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_STATISTICS(\"constants\")" ] }, { "cell_type": "code", "execution_count": 87, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 87, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_STATISTICS(\"variables\")" ] }, { "cell_type": "code", "execution_count": 88, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 88, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_STATISTICS(\"properties\")" ] }, { "cell_type": "code", "execution_count": 89, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 89, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_STATISTICS(\"invariants\")" ] }, { "cell_type": "code", "execution_count": 90, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 90, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_STATISTICS(\"operations\")" ] }, { "cell_type": "code", "execution_count": 91, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 91, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_STATISTICS(\"static_assertions\")" ] }, { "cell_type": "code", "execution_count": 92, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0" ] }, "execution_count": 92, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_STATISTICS(\"dynamic_assertions\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### PROJECT_INFO\n", "This external function provides access to various information strings about the current specification being processed, with all auxiliary files (i.e., project).\n", "Type: $STRING \\rightarrow POW(STRING)$." ] }, { "cell_type": "code", "execution_count": 93, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "{\"manual\"}" ] }, "execution_count": 93, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"files\")" ] }, { "cell_type": "code", "execution_count": 100, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "{\"from_string\"}" ] }, "execution_count": 100, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"main-file\")" ] }, { "cell_type": "code", "execution_count": 94, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 94, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"variables\")" ] }, { "cell_type": "code", "execution_count": 95, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 95, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"constants\")" ] }, { "cell_type": "code", "execution_count": 96, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 96, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"sets\")" ] }, { "cell_type": "code", "execution_count": 97, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 97, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"operations\")" ] }, { "cell_type": "code", "execution_count": 98, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 98, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"assertion_labels\")" ] }, { "cell_type": "code", "execution_count": 99, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "∅" ] }, "execution_count": 99, "metadata": {}, "output_type": "execute_result" } ], "source": [ "PROJECT_INFO(\"invariant_labels\")" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## LibraryIO\n", "\n", "This library provides various input/output facilities.\n", "It is probably most useful for debugging, but can also be used to write B machines\n", "which can read and write data.\n", "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n", "\n", "`DEFINITIONS \"LibraryIO.def\"`\n", "\n", "The file `LibraryIO.def` is also bundled with ProB and can be found in the `stdlib` folder." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## LibraryXML\n", "\n", "This library provides various functions to read and write XML data from file and strings.\n", "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n", "\n", "`DEFINITIONS \"LibraryXML.def\"`\n", "\n", "The file `LibraryXML.def` is also bundled with ProB and can be found in the `stdlib` folder.\n", "\n", "### Internal Data Type\n", "\n", "An XML document is represented using the type seq(XML_ELement_Type), i.e., a sequence\n", " of XML elements, whose type is defined by the following (included in the LibraryXML.def file):\n", "\n", "`\n", " XML_ELement_Type == \n", " struct(\n", " recId: NATURAL1,\n", " pId:NATURAL,\n", " element:STRING,\n", " attributes: STRING +-> STRING,\n", " meta: STRING +-> STRING\n", " );\n", "`\n", "\n", "### Files and Strings\n", "\n", "XML documents can either be stored in a file or in a B string." ] }, { "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 }