From 1c17b3dcc5c3d5ddeec62f797edc54235e0a0ee7 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 17 Oct 2022 17:36:08 +0200
Subject: [PATCH] update notebook
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
sks/1_B_Sprache.ipynb | 936 ++++++++++++++++++++++++++++++++++++------
1 file changed, 818 insertions(+), 118 deletions(-)
diff --git a/sks/1_B_Sprache.ipynb b/sks/1_B_Sprache.ipynb
index 282ecf1..d381992 100644
--- a/sks/1_B_Sprache.ipynb
+++ b/sks/1_B_Sprache.ipynb
@@ -45,8 +45,12 @@
},
{
"cell_type": "code",
- "execution_count": 1,
- "metadata": {},
+ "execution_count": 15,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -57,7 +61,7 @@
"5"
]
},
- "execution_count": 1,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -76,7 +80,11 @@
{
"cell_type": "code",
"execution_count": 2,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -105,8 +113,12 @@
},
{
"cell_type": "code",
- "execution_count": 3,
- "metadata": {},
+ "execution_count": 25,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -117,7 +129,7 @@
"{FALSE}"
]
},
- "execution_count": 3,
+ "execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
@@ -135,8 +147,12 @@
},
{
"cell_type": "code",
- "execution_count": 4,
- "metadata": {},
+ "execution_count": 20,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -147,7 +163,7 @@
"{FALSE}"
]
},
- "execution_count": 4,
+ "execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@@ -163,31 +179,68 @@
"## Syntax\n",
"\n",
"Die meisten Operatoren in B können entweder als ASCII Zeichenkette oder als Unicode Symbol eingegeben werden.\n",
- "Die Syntax von Event-B und klassischem B unterscheidet sich leicht.\n",
- "In Rodin muss man Event-B Syntax verwenden; Jupyter verwendet momentan nur klassisches B.\n",
- "\n",
- "Zum Beispiel benutzt Rodin `^` zum Potenzieren, während man im klassische B `**` verwendet:"
+ "Hier verwenden wir zum Beispiel die Unicode Version von ```/``` für die Division:"
]
},
{
"cell_type": "code",
- "execution_count": 5,
- "metadata": {},
+ "execution_count": 4,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
"text/markdown": [
- "$1267650600228229401496703205376$"
+ "$5$"
],
"text/plain": [
- "1267650600228229401496703205376"
+ "5"
]
},
- "execution_count": 5,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
+ "source": [
+ "10 ÷ 2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "Die Syntax von Event-B und klassischem B unterscheidet sich leicht.\n",
+ "In Rodin muss man Event-B Syntax verwenden; Jupyter verwendet standardmäßig klassisches B.\n",
+ "\n",
+ "Zum Beispiel benutzt Rodin `^` zum Potenzieren, während man im klassische B `**` verwendet:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: ERROR\nProB returned error messages:\nError: Type mismatch: Expected POW(_A), but was INTEGER in '2'\nError: Type mismatch: Expected POW(_A), but was INTEGER in '100'",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mERROR\u001b[0m",
+ "\u001b[1m\u001b[30m2 errors:\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected POW(_A), but was INTEGER in '2'\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected POW(_A), but was INTEGER in '100'\u001b[0m"
+ ]
+ }
+ ],
"source": [
"2**100"
]
@@ -199,13 +252,19 @@
"In Rodin wird `**` für das kartesische Produkt verwendet, im klassischen B verwendet man dafür `*`.\n",
"Wir laden jetzt ein leeres Event-B Modell um den Parser in den Event-B Modus zu wechseln.\n",
"Man kann auch das Kommando ```:language event_b``` verwenden um den Parser umzustellen.\n",
- "Mit ```:language classical_b``` kann man zurück zum normalen B Parser wechseln."
+ "Mit ```:language classical_b``` kann man zurück zum normalen B Parser wechseln.\n",
+ "Wenn man eine B Maschine oder einen Kontext lädt wechselt der Parser in den richtigen Modus.\n",
+ "Hier laden wir einen leeren Event-B Kontext; dadurch wechselt der Parser in den Event-B Modus:"
]
},
{
"cell_type": "code",
- "execution_count": 8,
- "metadata": {},
+ "execution_count": 27,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -213,7 +272,7 @@
"Loaded machine: empty_ctx"
]
},
- "execution_count": 8,
+ "execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
@@ -224,8 +283,12 @@
},
{
"cell_type": "code",
- "execution_count": 10,
- "metadata": {},
+ "execution_count": 30,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -236,7 +299,7 @@
"1267650600228229401496703205376"
]
},
- "execution_count": 10,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -279,8 +342,12 @@
},
{
"cell_type": "code",
- "execution_count": 11,
- "metadata": {},
+ "execution_count": 31,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -291,7 +358,7 @@
"¬(2 > 3 ∨ 4 > 2) ⇔ 5 > 2"
]
},
- "execution_count": 11,
+ "execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
@@ -309,8 +376,12 @@
},
{
"cell_type": "code",
- "execution_count": 12,
- "metadata": {},
+ "execution_count": 32,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -321,19 +392,23 @@
"FALSE"
]
},
- "execution_count": 12,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "not(2>3 or 4>2) <=> 5>2"
+ "not(2>3 or 4>2) ⇔ 5>2"
]
},
{
"cell_type": "code",
"execution_count": 13,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -356,7 +431,11 @@
{
"cell_type": "code",
"execution_count": 14,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -379,7 +458,11 @@
{
"cell_type": "code",
"execution_count": 15,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -412,8 +495,12 @@
},
{
"cell_type": "code",
- "execution_count": 22,
- "metadata": {},
+ "execution_count": 33,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -424,7 +511,7 @@
"FALSE"
]
},
- "execution_count": 22,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -435,8 +522,12 @@
},
{
"cell_type": "code",
- "execution_count": 23,
- "metadata": {},
+ "execution_count": 34,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -447,7 +538,7 @@
"TRUE"
]
},
- "execution_count": 23,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
@@ -459,7 +550,11 @@
{
"cell_type": "code",
"execution_count": 24,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -481,8 +576,12 @@
},
{
"cell_type": "code",
- "execution_count": 25,
- "metadata": {},
+ "execution_count": 35,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -493,7 +592,7 @@
"FALSE"
]
},
- "execution_count": 25,
+ "execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
@@ -514,8 +613,12 @@
},
{
"cell_type": "code",
- "execution_count": 26,
- "metadata": {},
+ "execution_count": 39,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"ename": "EvaluationException",
@@ -553,8 +656,12 @@
},
{
"cell_type": "code",
- "execution_count": 29,
- "metadata": {},
+ "execution_count": 42,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -565,7 +672,7 @@
"TRUE"
]
},
- "execution_count": 29,
+ "execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
@@ -574,6 +681,33 @@
"true or false"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "⊤ or ⊥"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -589,7 +723,11 @@
{
"cell_type": "code",
"execution_count": 30,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -611,8 +749,12 @@
},
{
"cell_type": "code",
- "execution_count": 31,
- "metadata": {},
+ "execution_count": 43,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -623,7 +765,7 @@
"TRUE"
]
},
- "execution_count": 31,
+ "execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@@ -635,7 +777,11 @@
{
"cell_type": "code",
"execution_count": 32,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -663,16 +809,23 @@
"\n",
"In B gibt es zwei Quantoren die neue Variablen einführen:\n",
"* den Existenzquantor (mindestens eins)\n",
- " - #x.(P) ∃x.(P)\n",
+ " - #x.(P) als ASCII\n",
+ " - ∃x.(P) als Unicode\n",
"* den Allquantor/Universalquantor (alle / jeder)\n",
- " - !x.(P => Q) ∀(x).(P ⇒ Q)\n",
- " "
+ " - !x.(P => Q) als ASCII\n",
+ " - ∀(x).(P ⇒ Q) als Unicode\n",
+ " \n",
+ " Der Rumpf eines Allquantors muss also immer eine Implikation auf oberster Ebene verwenden."
]
},
{
"cell_type": "code",
- "execution_count": 33,
- "metadata": {},
+ "execution_count": 44,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -683,7 +836,7 @@
"TRUE"
]
},
- "execution_count": 33,
+ "execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
@@ -694,8 +847,12 @@
},
{
"cell_type": "code",
- "execution_count": 34,
- "metadata": {},
+ "execution_count": 45,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -712,7 +869,7 @@
"\tx = 3"
]
},
- "execution_count": 34,
+ "execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
@@ -723,8 +880,12 @@
},
{
"cell_type": "code",
- "execution_count": 35,
- "metadata": {},
+ "execution_count": 46,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -741,7 +902,7 @@
"\tx = 3"
]
},
- "execution_count": 35,
+ "execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
@@ -752,7 +913,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -783,7 +944,37 @@
"* Bei Quantoren, zum Beispiel, müssen die neuen Variablen typisiert werden\n",
" - ∃x.(2>3) ist nicht erlaubt\n",
"\n",
- "Generell: für ∃x.(P) und ∀(x).(P ⇒ Q) muss P den Typen von x bestimmbar machen"
+ "Generell: für ∃x.(P) und ∀(x).(P ⇒ Q) muss P den Typen von x bestimmbar machen.\n",
+ "Deshalb ist der Rumpf eines Allquantors auch immer eine Implikation.\n",
+ " Beim Existenzquantor wird oft eine Konjunktion verwendet.\n",
+ " Warum macht eine Implikation beim Existenzquantor fast nie Sinn?"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 49,
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 49,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "∃x.(x>-100000 => 22=1)"
]
},
{
@@ -810,7 +1001,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -833,7 +1024,7 @@
},
{
"cell_type": "code",
- "execution_count": 41,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -867,8 +1058,12 @@
},
{
"cell_type": "code",
- "execution_count": 42,
- "metadata": {},
+ "execution_count": 51,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -879,7 +1074,7 @@
"1"
]
},
- "execution_count": 42,
+ "execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
@@ -890,7 +1085,7 @@
},
{
"cell_type": "code",
- "execution_count": 43,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -993,7 +1188,7 @@
},
{
"cell_type": "code",
- "execution_count": 46,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -1023,7 +1218,7 @@
},
{
"cell_type": "code",
- "execution_count": 47,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -1046,19 +1241,23 @@
},
{
"cell_type": "code",
- "execution_count": 48,
- "metadata": {},
+ "execution_count": 53,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
"text/markdown": [
- "$\\{\\mathit{x}\\mid \\mathit{x} > 4\\}$"
+ "$\\{\\mathit{x}\\mid\\mathit{x} > 4\\}$"
],
"text/plain": [
"{x∣x > 4}"
]
},
- "execution_count": 48,
+ "execution_count": 53,
"metadata": {},
"output_type": "execute_result"
}
@@ -1209,7 +1408,11 @@
{
"cell_type": "code",
"execution_count": 54,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1397,6 +1600,40 @@
"NAT = {x | x>=0 }"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "In Event-B gibt es auch eine angepasste Variante der Notation `{x . P | E}`, wo man einen Ausdruck `E` angibt der in die generierte Menge eingefügt wird:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 76,
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,4,9,16,25,36,49,64,81,100\\}$"
+ ],
+ "text/plain": [
+ "{1,4,9,16,25,36,49,64,81,100}"
+ ]
+ },
+ "execution_count": 76,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x.x:1..10|x*x}"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -1412,25 +1649,36 @@
},
{
"cell_type": "code",
- "execution_count": 65,
- "metadata": {},
+ "execution_count": 58,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
"text/latex": [
- "$\\{1,2,3\\} \\not\\subset \\{1,2,3\\}$"
+ "$\\neg (\\{1,2,3\\} \\not\\subset \\{1,2,3\\})$"
],
"text/plain": [
- "{1,2,3} ⊄ {1,2,3}"
+ "¬({1,2,3} ⊄ {1,2,3})"
]
},
- "execution_count": 65,
+ "execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":prettyprint {1,2,3} /<<: {1,2,3}"
+ ":prettyprint not({1,2,3} /<<: {1,2,3})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Zusätzlich hat Event-B das partition Prädikat, welches wir weiter unter erklären."
]
},
{
@@ -1451,8 +1699,12 @@
},
{
"cell_type": "code",
- "execution_count": 66,
- "metadata": {},
+ "execution_count": 59,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1475,20 +1727,24 @@
"\taub1 = {1,2,3,4}"
]
},
- "execution_count": 66,
+ "execution_count": 59,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "a = {1,2,4} & b = {2,3,4} & aub1 = a ∪ b &\n",
+ "a = {1,2,4} & b = {2,3,4} & aub1 = a \\/ b &\n",
"aub2 = {x | x:a or x:b}"
]
},
{
"cell_type": "code",
- "execution_count": 67,
- "metadata": {},
+ "execution_count": 60,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1511,7 +1767,7 @@
"\taib1 = {2,4}"
]
},
- "execution_count": 67,
+ "execution_count": 60,
"metadata": {},
"output_type": "execute_result"
}
@@ -1523,8 +1779,12 @@
},
{
"cell_type": "code",
- "execution_count": 68,
- "metadata": {},
+ "execution_count": 61,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1547,20 +1807,51 @@
"\taib1 = {1}"
]
},
- "execution_count": 68,
+ "execution_count": 61,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "a = {1,2,4} & b = {2,3,4} & aib1 = a \\b \n",
+ "a = {1,2,4} & b = {2,3,4} & aib1 = a \\ b \n",
"& aib2 = {x | x:a & x/:b}"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 70,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,4,9,16,25,36,49,64,81,100\\}$"
+ ],
+ "text/plain": [
+ "{1,4,9,16,25,36,49,64,81,100}"
+ ]
+ },
+ "execution_count": 70,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x.x:1..10|x*x}"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 69,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1594,8 +1885,12 @@
},
{
"cell_type": "code",
- "execution_count": 70,
- "metadata": {},
+ "execution_count": 68,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1606,7 +1901,7 @@
"{∅,{1},{1,2},{2}}"
]
},
- "execution_count": 70,
+ "execution_count": 68,
"metadata": {},
"output_type": "execute_result"
}
@@ -1703,7 +1998,7 @@
},
{
"cell_type": "code",
- "execution_count": 74,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -1753,7 +2048,7 @@
},
{
"cell_type": "code",
- "execution_count": 75,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -1803,7 +2098,7 @@
},
{
"cell_type": "code",
- "execution_count": 76,
+ "execution_count": null,
"metadata": {},
"outputs": [
{
@@ -1854,8 +2149,12 @@
},
{
"cell_type": "code",
- "execution_count": 77,
- "metadata": {},
+ "execution_count": 71,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1886,7 +2185,7 @@
"\tO = 0"
]
},
- "execution_count": 77,
+ "execution_count": 71,
"metadata": {},
"output_type": "execute_result"
}
@@ -1907,22 +2206,26 @@
},
{
"cell_type": "code",
- "execution_count": 79,
- "metadata": {},
+ "execution_count": 73,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
"text/markdown": [
"|S|E|N|D|M|O|R|Y|\n",
"|---|---|---|---|---|---|---|---|\n",
- "|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|\n"
+ "|9|5|6|7|1|0|8|2|\n"
],
"text/plain": [
"S\tE\tN\tD\tM\tO\tR\tY\n",
"9\t5\t6\t7\t1\t0\t8\t2\n"
]
},
- "execution_count": 79,
+ "execution_count": 73,
"metadata": {},
"output_type": "execute_result"
}
@@ -1935,6 +2238,113 @@
" = M*10000 + O*1000 + N*100 + E*10 + Y }"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Das Partition Prädikat\n",
+ "\n",
+ "Dieses Prädikat gibt es nur in Event-B und es ist syntaktischer Zucker für einen grösseren äquivalenten Ausdruck:\n",
+ "```\n",
+ " partition(S,S1,S2,...,Sn)\n",
+ " ```\n",
+ " steht für\n",
+ " ```\n",
+ " S = S1 \\/ S2 \\/ ... Sn &\n",
+ " S1 /\\ S2 = {} & ... S1 /\\ Sn = {} &\n",
+ " S2 /\\ S3 = {} & ... S2 /\\ Sn = {}\n",
+ " ...\n",
+ " Sn-1 /\\ Sn = {}\n",
+ " ```"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed language for user input to Event-B (forced)"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language event_b"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "partition(1..3,{1},{2},{3})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 74,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|a|b|\n",
+ "|---|---|\n",
+ "|∅|{1,2}|\n",
+ "|{1}|{2}|\n",
+ "|{1,2}|∅|\n",
+ "|{2}|{1}|\n"
+ ],
+ "text/plain": [
+ "a\tb\n",
+ "{}\t{1,2}\n",
+ "{1}\t{2}\n",
+ "{1,2}\t{}\n",
+ "{2}\t{1}\n"
+ ]
+ },
+ "execution_count": 74,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {a|->b| partition(1..2,a,b)}"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -1979,7 +2389,11 @@
{
"cell_type": "code",
"execution_count": 80,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -1999,7 +2413,11 @@
{
"cell_type": "code",
"execution_count": 81,
- "metadata": {},
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
"outputs": [
{
"data": {
@@ -2169,10 +2587,292 @@
"\n"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Kleine Beispiele"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 1,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 2$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 2"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1+x=3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed language for user input to Event-B (forced)"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language event_b"
+ ]
+ },
+ {
+ "cell_type": "markdown",
"metadata": {},
+ "source": [
+ "Wenn man die Menge der Primzahlen so definiert, behält ProB diese als symbolische Menge:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\limp}{\\mathbin\\Rightarrow}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{Primzahlen} = /*@\\mathit{symbolic}*/ \\{\\mathit{x}\\mid\\mathit{x} > 1 \\land \\forall\\mathit{y}\\qdot(\\mathit{y} \\in 2 \\upto \\mathit{x} - 1 \\limp \\mathit{x} \\mathit{mod} \\mathit{y} > 0)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tPrimzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Man kann aber zum Beispiel eine Primzahl generieren:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\limp}{\\mathbin\\Rightarrow}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 2$\n",
+ "* $\\mathit{Primzahlen} = /*@\\mathit{symbolic}*/ \\{\\mathit{x}\\mid\\mathit{x} > 1 \\land \\forall\\mathit{y}\\qdot(\\mathit{y} \\in 2 \\upto \\mathit{x} - 1 \\limp \\mathit{x} \\mathit{mod} \\mathit{y} > 0)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 2\n",
+ "\tPrimzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x∈Primzahlen ∧ Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Man kann die Menge der Primzahlen auch mit 1..100 schneiden um die Primzahlen bis 100 zu bekommen:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\limp}{\\mathbin\\Rightarrow}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{res} = \\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97\\}$\n",
+ "* $\\mathit{Primzahlen} = /*@\\mathit{symbolic}*/ \\{\\mathit{x}\\mid\\mathit{x} > 1 \\land \\forall\\mathit{y}\\qdot(\\mathit{y} \\in 2 \\upto \\mathit{x} - 1 \\limp \\mathit{x} \\mathit{mod} \\mathit{y} > 0)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tres = {2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97}\n",
+ "\tPrimzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧\n",
+ "res = Primzahlen ∩ 1..100"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Hier rechnen wir jetzt die Anzahl der Primzahle bis 1000 aus:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\limp}{\\mathbin\\Rightarrow}\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{res} = 168$\n",
+ "* $\\mathit{Primzahlen} = /*@\\mathit{symbolic}*/ \\{\\mathit{x}\\mid\\mathit{x} > 1 \\land \\forall\\mathit{y}\\qdot(\\mathit{y} \\in 2 \\upto \\mathit{x} - 1 \\limp \\mathit{x} \\mathit{mod} \\mathit{y} > 0)\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tres = 168\n",
+ "\tPrimzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧\n",
+ "res = card(Primzahlen ∩ 1..1000)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|x|\n",
+ "|---|\n",
+ "|1|\n",
+ "|2|\n",
+ "|3|\n",
+ "|5|\n",
+ "|7|\n",
+ "|11|\n",
+ "|13|\n",
+ "|17|\n",
+ "|19|\n"
+ ],
+ "text/plain": [
+ "x\n",
+ "1\n",
+ "2\n",
+ "3\n",
+ "5\n",
+ "7\n",
+ "11\n",
+ "13\n",
+ "17\n",
+ "19\n"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {x|x:1..20 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
"outputs": [],
"source": []
}
@@ -2191,5 +2891,5 @@
}
},
"nbformat": 4,
- "nbformat_minor": 2
+ "nbformat_minor": 4
}
--
GitLab