Extract relevant parts of chapter 0 notebooks into syntax overview

413c189a · dgelessus · 3d42ab56 · 413c189a · 413c189a
Commit 413c189a authored 2 years ago by dgelessus
--- a/info4/kapitel-1/Syntax-Übersicht ProB-Notebooks.ipynb
+++ b/info4/kapitel-1/Syntax-Übersicht ProB-Notebooks.ipynb
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "c8417dbc",
+   "metadata": {},
+   "source": [
+    "# Jupyter-Notebooks mit ProB\n",
+    "\n",
+    "Einige Begleitmaterialien zur Vorlesung werden hier als [Jupyter](https://jupyter.org/)-Notebooks mit interaktiv ausführbaren Code-Abschnitten bereitgestellt.\n",
+    "Jupyter ist Ihnen evtl. bereits aus anderen Veranstaltungen bekannt oder wird Ihnen dort noch begegnen.\n",
+    "\n",
+    "Üblicherweise werden Jupyter-Notebooks mit Python programmiert.\n",
+    "Die Notebooks zu dieser Vorlesung verwenden stattdessen das Werkzeug [ProB](https://prob.hhu.de/w/),\n",
+    "welches mit der Sprache B arbeitet.\n",
+    "\n",
+    "[![ProB](img/prob_logo.png)](https://prob.hhu.de/w/)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "4f3ac800",
+   "metadata": {},
+   "source": [
+    "## Verwendung\n",
+    "\n",
+    "Sie können die Notebooks in Ihrem Browser mit Binder betrachten und ausführen (der erste Start dauert evtl. etwas länger):\n",
+    "\n",
+    "[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2F)\n",
+    "\n",
+    "Sofern Sie Jupyter auf Ihrem System installiert haben,\n",
+    "können Sie auch den [Jupyter-Kernel für ProB](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel#downloads) lokal installieren und mit [dem Notebook-Repository](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) verwenden:\n",
+    "\n",
+    "```sh\n",
+    "$ java -jar prob2-jupyter-kernel-1.3.0-all.jar install --user\n",
+    "$ git clone https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks.git\n",
+    "$ cd prob-teaching-notebooks\n",
+    "$ cd info4\n",
+    "$ jupyter notebook\n",
+    "```"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "b190c072",
+   "metadata": {},
+   "source": [
+    "## Syntax"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "2f86ef55",
+   "metadata": {},
+   "source": [
+    "Die B-Sprache,\n",
+    "die in diesen Notebooks verwendet wird,\n",
+    "unterstützt mathematische Syntax und basiert auf Prädikatenlogik und Mengenlehre.\n",
+    "In den meisten Fällen ist die Syntax identisch zu den Schreibweisen aus der Vorlesung und dem Skript,\n",
+    "aber in manchen Aspekten unterscheidet sich die B-Syntax.\n",
+    "Diese Unterschiede werden hier kurz zusammengefasst."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "752872b2",
+   "metadata": {},
+   "source": [
+    "Eingaben werden standardmäßig als mathematischer Ausdruck oder als Prädikat ausgewertet:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "8444c3f8",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$7$"
+      ],
+      "text/plain": [
+       "7"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "1 + 2*3"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "8c3d850e",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "2*3 < 4"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "c40a8fbb",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "{2*3, 5} ⊆ 3..6"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "9272586e",
+   "metadata": {},
+   "source": [
+    "An manchen Stellen verwenden die Notebooks spezielle Kommandos für ProB,\n",
+    "die mit `:` anfangen,\n",
+    "z. B. `:pref`.\n",
+    "Diese Zeilen können Sie ignorieren."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "id": "234c4b5b",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Preference changed: OPTIMIZE_AST = FALSE\n"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":pref OPTIMIZE_AST=FALSE"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "624691a7",
+   "metadata": {},
+   "source": [
+    "### Variablen"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "7ec9cf6c",
+   "metadata": {},
+   "source": [
+    "Wenn ProB ein Prädikat auswertet,\n",
+    "wird automatisch nach einer Lösung für alle offenen Variablen gesucht,\n",
+    "sodass das Prädikat wahr ist.\n",
+    "Z. B. wird $x<5$ interpretiert als $\\exists x . x<5$:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "id": "a824b43d",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{x} = 0$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tx = 0"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x<5"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "26577070",
+   "metadata": {},
+   "source": [
+    "Die gefundenen Lösungswerte werden nicht über Eingaben hinweg gespeichert,\n",
+    "sondern jedes Mal neu belegt:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "id": "e010e8ea",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{x} = 1$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tx = 1"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x=1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "id": "2787f25a",
+   "metadata": {},
+   "outputs": [
+    {
+     "ename": "CommandExecutionException",
+     "evalue": ":eval: Computation not completed: Unknown identifier \"x\"",
+     "output_type": "error",
+     "traceback": [
+      "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"x\"\u001b[0m"
+     ]
+    }
+   ],
+   "source": [
+    "x"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "4357082f",
+   "metadata": {},
+   "source": [
+    "Mit dem Befehl `:let` können Variablenwerte dauerhaft zugewiesen werden:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "id": "4b978071",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1$"
+      ],
+      "text/plain": [
+       "1"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let x 1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "id": "20d3e677",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x = 1"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "id": "80cd003c",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x = 2"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "0eb8b0df",
+   "metadata": {},
+   "source": [
+    "`:unlet` entfernt eine gespeicherte Variable wieder:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "id": "5b52c450",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    ":unlet x"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "68631aff",
+   "metadata": {},
+   "source": [
+    "### Prädikate"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "9461e3b3",
+   "metadata": {},
+   "source": [
+    "Das Argument vom Negationsoperator $\\lnot$ muss immer explizit geklammert werden:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "id": "ce29cca1",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "¬(1<2)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "ec281282",
+   "metadata": {},
+   "source": [
+    "ProB unterstützt keine aussagenlogischen Variablen -\n",
+    "der Wahrheitswert eines Prädikats kann also nicht direkt einer Variable zugewiesen werden:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "id": "847538f9",
+   "metadata": {},
+   "outputs": [
+    {
+     "ename": "EvaluationException",
+     "evalue": "expecting: 'symbolic', ')', ',', ';', double vertical bar",
+     "output_type": "error",
+     "traceback": [
+      "\u001b[1m\u001b[31mde.prob.animator.domainobjects.EvaluationException: expecting: 'symbolic', ')', ',', ';', double vertical bar\u001b[0m"
+     ]
+    }
+   ],
+   "source": [
+    "a=(1<2) ∧ a"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "8514048e",
+   "metadata": {},
+   "source": [
+    "Wenn ein Wahrheitswert als Variable behandelt werden soll,\n",
+    "muss er explizit mit dem Operator `bool` zu einem Boole'schen Datenwert konvertiert werden.\n",
+    "Solche Variablen können wiederum nicht direkt in Prädikaten verwendet werden,\n",
+    "sondern müssen explizit mit `TRUE` verglichen werden:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "id": "d89387e9",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{a} = \\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\ta = TRUE"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "a=bool(1<2) ∧ a=TRUE"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "a3a5d616",
+   "metadata": {},
+   "source": [
+    "### Mengen"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "f1096c22",
+   "metadata": {},
+   "source": [
+    "ProB erfordert, dass alle Mengen homogen sind.\n",
+    "Zwei Elemente derselben Menge dürfen keine unterschiedlichen Typen haben:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "id": "b9ddcb78",
+   "metadata": {},
+   "outputs": [
+    {
+     "ename": "CommandExecutionException",
+     "evalue": ":eval: Computation not completed: Type mismatch: Expected INTEGER, but was POW(INTEGER) in '{1}'",
+     "output_type": "error",
+     "traceback": [
+      "\u001b[1m\u001b[31m:eval: Computation not completed: Type mismatch: Expected INTEGER, but was POW(INTEGER) in '{1}'\u001b[0m"
+     ]
+    }
+   ],
+   "source": [
+    "{1, {1}}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "988f2ef1",
+   "metadata": {},
+   "source": [
+    "Die Kardinalität einer Menge, $|A|$, wird in B als $\\mathrm{card}(A)$ geschrieben:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "id": "db9fc40c",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$0$"
+      ],
+      "text/plain": [
+       "0"
+      ]
+     },
+     "execution_count": 16,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "card(∅)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "id": "7197e767",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$1$"
+      ],
+      "text/plain": [
+       "1"
+      ]
+     },
+     "execution_count": 17,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "card({0})"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "id": "24045156",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$2$"
+      ],
+      "text/plain": [
+       "2"
+      ]
+     },
+     "execution_count": 18,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "card({3,5})"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "d661f927",
+   "metadata": {},
+   "source": [
+    "Die Potenzmenge einer Menge wird $\\mathbb{P}(A)$ geschrieben:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 19,
+   "id": "d7c9f328",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\{\\emptyset,\\{1\\},\\{1,2\\},\\{2\\}\\}$"
+      ],
+      "text/plain": [
+       "{∅,{1},{1,2},{2}}"
+      ]
+     },
+     "execution_count": 19,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "ℙ({1,2})"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "66b4d0d2",
+   "metadata": {},
+   "source": [
+    "### Paare und Abbildungen"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "c9220354",
+   "metadata": {},
+   "source": [
+    "Paare werden in B oft als $x \\mapsto y$ anstatt $(x, y)$ dargestellt.\n",
+    "Beide Schreibweisen haben die gleiche Bedeutung."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "id": "f16024de",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$(1\\mapsto 2)$"
+      ],
+      "text/plain": [
+       "(1↦2)"
+      ]
+     },
+     "execution_count": 20,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "(1, 2)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "567f0f79",
+   "metadata": {},
+   "source": [
+    "Funktionen werden in B als Relationen, bzw. Mengen von Paaren, dargestellt:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 21,
+   "id": "8890cb60",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(2\\mapsto 1),(4\\mapsto 2),(6\\mapsto 3),(8\\mapsto 4),(10\\mapsto 5)\\}$"
+      ],
+      "text/plain": [
+       "{(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)}"
+      ]
+     },
+     "execution_count": 21,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let halb {a,b | a∈1..10 ∧ b∈1..10 & b*2=a}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 22,
+   "id": "3ae95bab",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$2$"
+      ],
+      "text/plain": [
+       "2"
+      ]
+     },
+     "execution_count": 22,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "halb(4)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "cb5d4125",
+   "metadata": {},
+   "source": [
+    "Der Definitionsbereich (englisch \"domain\") wird geschrieben als $\\mathrm{dom}(f)$,\n",
+    "der Wertebereich (Bildmenge, englisch \"range\") als $\\mathrm{ran}(f)$:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 23,
+   "id": "0e09a84a",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{2,4,6,8,10\\}$"
+      ],
+      "text/plain": [
+       "{2,4,6,8,10}"
+      ]
+     },
+     "execution_count": 23,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "dom(halb)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 24,
+   "id": "0af4cfe7",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{1,2,3,4,5\\}$"
+      ],
+      "text/plain": [
+       "{1,2,3,4,5}"
+      ]
+     },
+     "execution_count": 24,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "ran(halb)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "77ad83ef",
+   "metadata": {},
+   "source": [
+    "Die Verkettung/Komposition von Funktionen wird $f ; g$ geschrieben anstatt $g \\circ f$.\n",
+    "Achtung: Die Reihenfolge der beiden Funktionen ist hier umgekehrt!"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 25,
+   "id": "5a54d02e",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(1\\mapsto 2),(2\\mapsto 3),(3\\mapsto 4),(4\\mapsto 5),(5\\mapsto 6),(6\\mapsto 7),(7\\mapsto 8),(8\\mapsto 9),(9\\mapsto 10)\\}$"
+      ],
+      "text/plain": [
+       "{(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10)}"
+      ]
+     },
+     "execution_count": 25,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let inc {x,y | x∈1..10 ∧ y∈1..10 ∧ y=x+1}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "id": "1241d6d8",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 26,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "(halb ; inc)(4) = inc(halb(4))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 27,
+   "id": "a99755aa",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 27,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "(inc ; halb)(1) = halb(inc(1))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "f21c0259",
+   "metadata": {},
+   "source": [
+    "$f^n$ wird $\\mathrm{iterate}(f, n)$ geschrieben:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "id": "db7ef9ce",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 28,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "iterate(halb, 2)(8) = halb(halb(8))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "fcc7511f",
+   "metadata": {},
+   "source": [
+    "### Alphabete, Wörter, Sprachen"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "a4b9c92e",
+   "metadata": {},
+   "source": [
+    "Manche Definitionen geben wir in einem `MACHINE`-Block vor,\n",
+    "z. B. die Symbole eines Alphabets.\n",
+    "Sie müssen diese Syntax nicht näher verstehen."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 29,
+   "id": "e647c198",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Alphabet"
+      ]
+     },
+     "execution_count": 29,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "MACHINE Alphabet\n",
+    "SETS Σ = {a,b,c}\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 30,
+   "id": "cdbc267f",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Preference changed: PP_SEQUENCES = TRUE\n"
+      ]
+     },
+     "execution_count": 30,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":pref PP_SEQUENCES=TRUE"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "56267c5e",
+   "metadata": {},
+   "source": [
+    "Wörter werden hier explizit als Sequenz von Symbolen geschrieben,\n",
+    "z. B. $[c,b,a]$ anstatt $cba$.\n",
+    "Die Menge aller Wörter über ein Alphabet wird $\\mathrm{seq}(\\Sigma)$ anstatt $\\Sigma^*$ geschrieben:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 31,
+   "id": "f54776db",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 31,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "[a,a] ∈ seq(Σ)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "d21cc56b",
+   "metadata": {},
+   "source": [
+    "Das leere Wort wird als $[]$ dargestellt (da $\\lambda$ in B bereits eine andere Bedeutung hat):"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 32,
+   "id": "4590adc6",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 32,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "[] ∈ seq(Σ)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "cefb7b6c",
+   "metadata": {},
+   "source": [
+    "B behandelt Sequenzen intern als Mengen von Paaren $\\mathit{index} \\mapsto \\mathit{value}$,\n",
+    "wie in Kapitel 1 der Vorlesung vorgestellt.\n",
+    "Diese Darstellung ist in den Notebooks allerdings normalerweise nicht sichtbar."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 33,
+   "id": "2252b6db",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$[\\mathit{a},\\mathit{b}]$"
+      ],
+      "text/plain": [
+       "[a,b]"
+      ]
+     },
+     "execution_count": 33,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "{1↦a, 2↦b}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "47111cf0",
+   "metadata": {},
+   "source": [
+    "Konkatenation erfolgt explizit mit dem Operator `^`:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 34,
+   "id": "d96e0212",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{w} = [\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]$\n",
+       "* $\\mathit{x} = [\\mathit{a},\\mathit{a}]$\n",
+       "* $\\mathit{y} = [\\mathit{b},\\mathit{c}]$"
+      ],
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tw = [a,a,b,c]\n",
+       "\tx = [a,a]\n",
+       "\ty = [b,c]"
+      ]
+     },
+     "execution_count": 34,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x = [a,a] & y = [b,c] & w = x ^ y"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "03143769",
+   "metadata": {},
+   "source": [
+    "Die Spiegelbildoperation wird $\\mathrm{rev}(u)$ anstatt $\\mathrm{sp}(u)$ geschrieben:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 35,
+   "id": "21e51f7f",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$[\\mathit{c},\\mathit{b},\\mathit{a}]$"
+      ],
+      "text/plain": [
+       "[c,b,a]"
+      ]
+     },
+     "execution_count": 35,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "rev([a,b,c])"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "ProB 2",
+   "language": "prob",
+   "name": "prob2"
+  },
+  "language_info": {
+   "codemirror_mode": "prob2_jupyter_repl",
+   "file_extension": ".prob",
+   "mimetype": "text/x-prob2-jupyter-repl",
+   "name": "prob"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
+%% Cell type:markdown id:c8417dbc tags:
+
+# Jupyter-Notebooks mit ProB
+
+Einige Begleitmaterialien zur Vorlesung werden hier als [Jupyter](https://jupyter.org/)-Notebooks mit interaktiv ausführbaren Code-Abschnitten bereitgestellt.
+Jupyter ist Ihnen evtl. bereits aus anderen Veranstaltungen bekannt oder wird Ihnen dort noch begegnen.
+
+Üblicherweise werden Jupyter-Notebooks mit Python programmiert.
+Die Notebooks zu dieser Vorlesung verwenden stattdessen das Werkzeug [ProB](https://prob.hhu.de/w/),
+welches mit der Sprache B arbeitet.
+
+[![ProB](img/prob_logo.png)](https://prob.hhu.de/w/)
+
+%% Cell type:markdown id:4f3ac800 tags:
+
+## Verwendung
+
+Sie können die Notebooks in Ihrem Browser mit Binder betrachten und ausführen (der erste Start dauert evtl. etwas länger):
+
+[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2F)
+
+Sofern Sie Jupyter auf Ihrem System installiert haben,
+können Sie auch den [Jupyter-Kernel für ProB](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel#downloads) lokal installieren und mit [dem Notebook-Repository](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) verwenden:
+
+```sh
+$ java -jar prob2-jupyter-kernel-1.3.0-all.jar install --user
+$ git clone https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks.git
+$ cd prob-teaching-notebooks
+$ cd info4
+$ jupyter notebook
+```
+
+%% Cell type:markdown id:b190c072 tags:
+
+## Syntax
+
+%% Cell type:markdown id:2f86ef55 tags:
+
+Die B-Sprache,
+die in diesen Notebooks verwendet wird,
+unterstützt mathematische Syntax und basiert auf Prädikatenlogik und Mengenlehre.
+In den meisten Fällen ist die Syntax identisch zu den Schreibweisen aus der Vorlesung und dem Skript,
+aber in manchen Aspekten unterscheidet sich die B-Syntax.
+Diese Unterschiede werden hier kurz zusammengefasst.
+
+%% Cell type:markdown id:752872b2 tags:
+
+Eingaben werden standardmäßig als mathematischer Ausdruck oder als Prädikat ausgewertet:
+
+%% Cell type:code id:8444c3f8 tags:
+
+``` prob
+1 + 2*3
+```
+
+%% Output
+
+    $7$
+    7
+
+%% Cell type:code id:8c3d850e tags:
+
+``` prob
+2*3 < 4
+```
+
+%% Output
+
+    $\mathit{FALSE}$
+    FALSE
+
+%% Cell type:code id:c40a8fbb tags:
+
+``` prob
+{2*3, 5} ⊆ 3..6
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    TRUE
+
+%% Cell type:markdown id:9272586e tags:
+
+An manchen Stellen verwenden die Notebooks spezielle Kommandos für ProB,
+die mit `:` anfangen,
+z. B. `:pref`.
+Diese Zeilen können Sie ignorieren.
+
+%% Cell type:code id:234c4b5b tags:
+
+``` prob
+:pref OPTIMIZE_AST=FALSE
+```
+
+%% Output
+
+    Preference changed: OPTIMIZE_AST = FALSE
+
+%% Cell type:markdown id:624691a7 tags:
+
+### Variablen
+
+%% Cell type:markdown id:7ec9cf6c tags:
+
+Wenn ProB ein Prädikat auswertet,
+wird automatisch nach einer Lösung für alle offenen Variablen gesucht,
+sodass das Prädikat wahr ist.
+Z. B. wird $x<5$ interpretiert als $\exists x . x<5$:
+
+%% Cell type:code id:a824b43d tags:
+
+``` prob
+x<5
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    
+    **Solution:**
+    * $\mathit{x} = 0$
+    TRUE
+    
+    Solution:
+    	x = 0
+
+%% Cell type:markdown id:26577070 tags:
+
+Die gefundenen Lösungswerte werden nicht über Eingaben hinweg gespeichert,
+sondern jedes Mal neu belegt:
+
+%% Cell type:code id:e010e8ea tags:
+
+``` prob
+x=1
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    
+    **Solution:**
+    * $\mathit{x} = 1$
+    TRUE
+    
+    Solution:
+    	x = 1
+
+%% Cell type:code id:2787f25a tags:
+
+``` prob
+x
+```
+
+%% Output
+
+    :eval: Computation not completed: Unknown identifier "x"
+
+%% Cell type:markdown id:4357082f tags:
+
+Mit dem Befehl `:let` können Variablenwerte dauerhaft zugewiesen werden:
+
+%% Cell type:code id:4b978071 tags:
+
+``` prob
+:let x 1
+```
+
+%% Output
+
+    $1$
+    1
+
+%% Cell type:code id:20d3e677 tags:
+
+``` prob
+x = 1
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    TRUE
+
+%% Cell type:code id:80cd003c tags:
+
+``` prob
+x = 2
+```
+
+%% Output
+
+    $\mathit{FALSE}$
+    FALSE
+
+%% Cell type:markdown id:0eb8b0df tags:
+
+`:unlet` entfernt eine gespeicherte Variable wieder:
+
+%% Cell type:code id:5b52c450 tags:
+
+``` prob
+:unlet x
+```
+
+%% Cell type:markdown id:68631aff tags:
+
+### Prädikate
+
+%% Cell type:markdown id:9461e3b3 tags:
+
+Das Argument vom Negationsoperator $\lnot$ muss immer explizit geklammert werden:
+
+%% Cell type:code id:ce29cca1 tags:
+
+``` prob
+¬(1<2)
+```
+
+%% Output
+
+    $\mathit{FALSE}$
+    FALSE
+
+%% Cell type:markdown id:ec281282 tags:
+
+ProB unterstützt keine aussagenlogischen Variablen -
+der Wahrheitswert eines Prädikats kann also nicht direkt einer Variable zugewiesen werden:
+
+%% Cell type:code id:847538f9 tags:
+
+``` prob
+a=(1<2) ∧ a
+```
+
+%% Output
+
+    de.prob.animator.domainobjects.EvaluationException: expecting: 'symbolic', ')', ',', ';', double vertical bar
+
+%% Cell type:markdown id:8514048e tags:
+
+Wenn ein Wahrheitswert als Variable behandelt werden soll,
+muss er explizit mit dem Operator `bool` zu einem Boole'schen Datenwert konvertiert werden.
+Solche Variablen können wiederum nicht direkt in Prädikaten verwendet werden,
+sondern müssen explizit mit `TRUE` verglichen werden:
+
+%% Cell type:code id:d89387e9 tags:
+
+``` prob
+a=bool(1<2) ∧ a=TRUE
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    
+    **Solution:**
+    * $\mathit{a} = \mathit{TRUE}$
+    TRUE
+    
+    Solution:
+    	a = TRUE
+
+%% Cell type:markdown id:a3a5d616 tags:
+
+### Mengen
+
+%% Cell type:markdown id:f1096c22 tags:
+
+ProB erfordert, dass alle Mengen homogen sind.
+Zwei Elemente derselben Menge dürfen keine unterschiedlichen Typen haben:
+
+%% Cell type:code id:b9ddcb78 tags:
+
+``` prob
+{1, {1}}
+```
+
+%% Output
+
+    :eval: Computation not completed: Type mismatch: Expected INTEGER, but was POW(INTEGER) in '{1}'
+
+%% Cell type:markdown id:988f2ef1 tags:
+
+Die Kardinalität einer Menge, $|A|$, wird in B als $\mathrm{card}(A)$ geschrieben:
+
+%% Cell type:code id:db9fc40c tags:
+
+``` prob
+card(∅)
+```
+
+%% Output
+
+    $0$
+    0
+
+%% Cell type:code id:7197e767 tags:
+
+``` prob
+card({0})
+```
+
+%% Output
+
+    $1$
+    1
+
+%% Cell type:code id:24045156 tags:
+
+``` prob
+card({3,5})
+```
+
+%% Output
+
+    $2$
+    2
+
+%% Cell type:markdown id:d661f927 tags:
+
+Die Potenzmenge einer Menge wird $\mathbb{P}(A)$ geschrieben:
+
+%% Cell type:code id:d7c9f328 tags:
+
+``` prob
+ℙ({1,2})
+```
+
+%% Output
+
+    $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$
+    {∅,{1},{1,2},{2}}
+
+%% Cell type:markdown id:66b4d0d2 tags:
+
+### Paare und Abbildungen
+
+%% Cell type:markdown id:c9220354 tags:
+
+Paare werden in B oft als $x \mapsto y$ anstatt $(x, y)$ dargestellt.
+Beide Schreibweisen haben die gleiche Bedeutung.
+
+%% Cell type:code id:f16024de tags:
+
+``` prob
+(1, 2)
+```
+
+%% Output
+
+    $(1\mapsto 2)$
+    (1↦2)
+
+%% Cell type:markdown id:567f0f79 tags:
+
+Funktionen werden in B als Relationen, bzw. Mengen von Paaren, dargestellt:
+
+%% Cell type:code id:8890cb60 tags:
+
+``` prob
+:let halb {a,b | a∈1..10 ∧ b∈1..10 & b*2=a}
+```
+
+%% Output
+
+    $\{(2\mapsto 1),(4\mapsto 2),(6\mapsto 3),(8\mapsto 4),(10\mapsto 5)\}$
+    {(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)}
+
+%% Cell type:code id:3ae95bab tags:
+
+``` prob
+halb(4)
+```
+
+%% Output
+
+    $2$
+    2
+
+%% Cell type:markdown id:cb5d4125 tags:
+
+Der Definitionsbereich (englisch "domain") wird geschrieben als $\mathrm{dom}(f)$,
+der Wertebereich (Bildmenge, englisch "range") als $\mathrm{ran}(f)$:
+
+%% Cell type:code id:0e09a84a tags:
+
+``` prob
+dom(halb)
+```
+
+%% Output
+
+    $\{2,4,6,8,10\}$
+    {2,4,6,8,10}
+
+%% Cell type:code id:0af4cfe7 tags:
+
+``` prob
+ran(halb)
+```
+
+%% Output
+
+    $\{1,2,3,4,5\}$
+    {1,2,3,4,5}
+
+%% Cell type:markdown id:77ad83ef tags:
+
+Die Verkettung/Komposition von Funktionen wird $f ; g$ geschrieben anstatt $g \circ f$.
+Achtung: Die Reihenfolge der beiden Funktionen ist hier umgekehrt!
+
+%% Cell type:code id:5a54d02e tags:
+
+``` prob
+:let inc {x,y | x∈1..10 ∧ y∈1..10 ∧ y=x+1}
+```
+
+%% Output
+
+    $\{(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 10)\}$
+    {(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10)}
+
+%% Cell type:code id:1241d6d8 tags:
+
+``` prob
+(halb ; inc)(4) = inc(halb(4))
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    TRUE
+
+%% Cell type:code id:a99755aa tags:
+
+``` prob
+(inc ; halb)(1) = halb(inc(1))
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    TRUE
+
+%% Cell type:markdown id:f21c0259 tags:
+
+$f^n$ wird $\mathrm{iterate}(f, n)$ geschrieben:
+
+%% Cell type:code id:db7ef9ce tags:
+
+``` prob
+iterate(halb, 2)(8) = halb(halb(8))
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    TRUE
+
+%% Cell type:markdown id:fcc7511f tags:
+
+### Alphabete, Wörter, Sprachen
+
+%% Cell type:markdown id:a4b9c92e tags:
+
+Manche Definitionen geben wir in einem `MACHINE`-Block vor,
+z. B. die Symbole eines Alphabets.
+Sie müssen diese Syntax nicht näher verstehen.
+
+%% Cell type:code id:e647c198 tags:
+
+``` prob
+MACHINE Alphabet
+SETS Σ = {a,b,c}
+END
+```
+
+%% Output
+
+    Loaded machine: Alphabet
+
+%% Cell type:code id:cdbc267f tags:
+
+``` prob
+:pref PP_SEQUENCES=TRUE
+```
+
+%% Output
+
+    Preference changed: PP_SEQUENCES = TRUE
+
+%% Cell type:markdown id:56267c5e tags:
+
+Wörter werden hier explizit als Sequenz von Symbolen geschrieben,
+z. B. $[c,b,a]$ anstatt $cba$.
+Die Menge aller Wörter über ein Alphabet wird $\mathrm{seq}(\Sigma)$ anstatt $\Sigma^*$ geschrieben:
+
+%% Cell type:code id:f54776db tags:
+
+``` prob
+[a,a] ∈ seq(Σ)
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    TRUE
+
+%% Cell type:markdown id:d21cc56b tags:
+
+Das leere Wort wird als $[]$ dargestellt (da $\lambda$ in B bereits eine andere Bedeutung hat):
+
+%% Cell type:code id:4590adc6 tags:
+
+``` prob
+[] ∈ seq(Σ)
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    TRUE
+
+%% Cell type:markdown id:cefb7b6c tags:
+
+B behandelt Sequenzen intern als Mengen von Paaren $\mathit{index} \mapsto \mathit{value}$,
+wie in Kapitel 1 der Vorlesung vorgestellt.
+Diese Darstellung ist in den Notebooks allerdings normalerweise nicht sichtbar.
+
+%% Cell type:code id:2252b6db tags:
+
+``` prob
+{1↦a, 2↦b}
+```
+
+%% Output
+
+    $[\mathit{a},\mathit{b}]$
+    [a,b]
+
+%% Cell type:markdown id:47111cf0 tags:
+
+Konkatenation erfolgt explizit mit dem Operator `^`:
+
+%% Cell type:code id:d96e0212 tags:
+
+``` prob
+x = [a,a] & y = [b,c] & w = x ^ y
+```
+
+%% Output
+
+    $\mathit{TRUE}$
+    
+    **Solution:**
+    * $\mathit{w} = [\mathit{a},\mathit{a},\mathit{b},\mathit{c}]$
+    * $\mathit{x} = [\mathit{a},\mathit{a}]$
+    * $\mathit{y} = [\mathit{b},\mathit{c}]$
+    TRUE
+    
+    Solution:
+    	w = [a,a,b,c]
+    	x = [a,a]
+    	y = [b,c]
+
+%% Cell type:markdown id:03143769 tags:
+
+Die Spiegelbildoperation wird $\mathrm{rev}(u)$ anstatt $\mathrm{sp}(u)$ geschrieben:
+
+%% Cell type:code id:21e51f7f tags:
+
+``` prob
+rev([a,b,c])
+```
+
+%% Output
+
+    $[\mathit{c},\mathit{b},\mathit{a}]$
+    [c,b,a]
--- a/info4/kapitel-1/img/prob_logo.png
+++ b/info4/kapitel-1/img/prob_logo.png