minor update

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

minor update
7641e3a9 · Michael Leuschel · 365232b5 · 7641e3a9
Commit 7641e3a9 authored 9 months ago by Michael Leuschel
--- a/sks/1_B_Sprache.ipynb
+++ b/sks/1_B_Sprache.ipynb
@@ -45,7 +45,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 2,
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
@@ -61,7 +61,7 @@
       "5"
      ]
     },
-     "execution_count": 15,
+     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -79,7 +79,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 3,
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
@@ -95,7 +95,7 @@
       "FALSE"
      ]
     },
-     "execution_count": 2,
+     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -113,7 +113,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": 4,
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
@@ -129,7 +129,7 @@
       "{FALSE}"
      ]
     },
-     "execution_count": 25,
+     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -147,7 +147,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 5,
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
@@ -163,7 +163,7 @@
       "{FALSE}"
      ]
     },
-     "execution_count": 20,
+     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -184,7 +184,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 6,
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
@@ -200,7 +200,7 @@
       "5"
      ]
     },
-     "execution_count": 4,
+     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -1328,16 +1328,17 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 51,
+   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
-     "ename": "CommandExecutionException",
+     "ename": "WithSourceCodeException",
-     "evalue": ":eval: NOT-WELL-DEFINED: \ncard applied to very large set, cardinality not representable in ProB:  closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(none)]))\n\n",
+     "evalue": "de.prob.exception.ProBError: NOT-WELL-DEFINED\nProB returned error messages:\nError: card applied to infinite set, cardinality not representable in ProB:  {x|x > 2} (:1:0 to 1:13)",
     "output_type": "error",
     "traceback": [
-      "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
+      "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-WELL-DEFINED\u001b[0m",
-      "\u001b[1m\u001b[31mcard applied to very large set, cardinality not representable in ProB:  closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(none)]))\u001b[0m"
+      "\u001b[1m\u001b[31mError: card applied to infinite set, cardinality not representable in ProB:  {x|x > 2} (:1:0 to 1:13)\u001b[0m",
+      "\u001b[1m\u001b[30m\u001b[0m\u001b[1m\u001b[30m\u001b[41mcard({x|x>2})\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
     ]
    }
   ],

 %% Cell type:markdown id: tags:
 # Vorlesung: B Sprache
 %% Cell type:markdown id: tags:
 ## Struktur von Event-B Modellen
 Ein Event-B System besteht aus
 * statischen Teilen: die Kontexte
 - definieren Konstanten, Basismengen, Axiome, Theoreme
 * dynamischen Teilen: Maschinen
 - definieren Variablen, Ereignisse, Invarianten
 * Kontexte können von Maschinen gesehen werden
 * Kontexte und Maschinen können verfeinert werden
 %% Cell type:markdown id: tags:
 ## Syntaktische Klassen
 Es gibt drei Arten von Formeln in B:
 - **Ausdrücke** (Expressions): haben einen Wert, verändern den Zustand einer B Maschine *nicht*
 - **Prädikate** (Predicates): sind wahr oder falsch, haben *keinen* Wert und verändern den Zustand der Maschine *nicht*
 - **Anweisungen** (Substitutions, Statements): haben keinen Wert, können aber den Zustand einer Maschine verändern
 Anweisungen sind zB `x := x+1` und können nur in Maschinen, nicht in Kontexten verwendet werden.
 %% Cell type:markdown id: tags:
 Dies ist ein Ausdruck in B:
 %% Cell type:code id: tags:
 ``` prob
 2+3
 ```
 %% Output
    $5$
    5
 %% Cell type:markdown id: tags:
 Dies ist ein Prädikat in B:
 %% Cell type:code id: tags:
 ``` prob
 2>3
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 B unterscheidet streng zwischen den Bool'schen Werten TRUE und FALSE und zwischen Prädikaten die wahr und falsch sind. Folgendes ist ein valider Ausdruck in B und beschreibt die Menge bestehend aus dem Bool'schen Wert `FALSE`:
 %% Cell type:code id: tags:
 ``` prob
 {FALSE}
 ```
 %% Output
    $\{\mathit{FALSE}\}$
    {FALSE}
 %% Cell type:markdown id: tags:
 Folgendes ist **kein** valider Ausdruck in B:
 %% Cell type:code id: tags:
 ``` prob
 {bool(2>3)}
 ```
 %% Output
    $\{\mathit{FALSE}\}$
    {FALSE}
 %% Cell type:markdown id: tags:
 ## Syntax
 Die meisten Operatoren in B können entweder als ASCII Zeichenkette oder als Unicode Symbol eingegeben werden.
 Hier verwenden wir zum Beispiel die Unicode Version von ```/``` für die Division:
 %% Cell type:code id: tags:
 ``` prob
 10 ÷ 2
 ```
 %% Output
    $5$
    5
 %% Cell type:markdown id: tags:
 Die Syntax von Event-B und klassischem B unterscheidet sich leicht.
 In Rodin muss man Event-B Syntax verwenden; Jupyter verwendet standardmäßig klassisches B.
 Zum Beispiel benutzt Rodin `^` zum Potenzieren, während man im klassische B `**` verwendet:
 %% Cell type:code id: tags:
 ``` prob
 2**100
 ```
 %% Output
    Error from ProB: ERROR
    2 errors:
    Error: Type mismatch: Expected POW(_A), but was INTEGER in '2'
    Error: Type mismatch: Expected POW(_A), but was INTEGER in '100'
 %% Cell type:markdown id: tags:
 In Rodin wird `**` für das kartesische Produkt verwendet, im klassischen B verwendet man dafür `*`.
 Wir laden jetzt ein leeres Event-B Modell um den Parser in den Event-B Modus zu wechseln.
 Man kann auch das Kommando ```:language event_b``` verwenden um den Parser umzustellen.
 Mit ```:language classical_b``` kann man zurück zum normalen B Parser wechseln.
 Wenn man eine B Maschine oder einen Kontext lädt wechselt der Parser in den richtigen Modus.
 Hier laden wir einen leeren Event-B Kontext; dadurch wechselt der Parser in den Event-B Modus:
 %% Cell type:code id: tags:
 ``` prob
 :load models/empty_ctx.eventb
 ```
 %% Output
    Loaded machine: empty_ctx
 %% Cell type:code id: tags:
 ``` prob
 2^100
 ```
 %% Output
    $1267650600228229401496703205376$
    1267650600228229401496703205376
 %% Cell type:markdown id: tags:
 ## Semantische Grundlage von B
 * Arithmetik (ganze Zahlen)  ÷   +   −   ≤
 * Prädikatenlogik  ⇒   ∀
 * Mengentheorie  ∩   ∪   ⊆   ∈
 * Paare
 * Relationen,Funktionen, Sequenzen/Folgen, Bäume
 %% Cell type:markdown id: tags:
 ## Aussagenlogik
 B unterstützt folgende Junktoren der Aussagenlogik:
 Junktor | ASCII | Unicode
 -------|-------|-----
 Konjunktion | & | ∧
 Disjunktion | or | ∨
 Negation | not | ¬
 Implikation | => | ⇒
 Äquivalenz | <=> | ⇔
 Mit `:prettyprint` kann man sich die Unicode Version einer Formel ausgeben lassen:
 %% Cell type:code id: tags:
 ``` prob
 :prettyprint not(2>3 or 4>2) <=> 5>2
 ```
 %% Output
    $\neg (2 > 3 \vee  4 > 2) \mathbin\Leftrightarrow  5 > 2$
    ¬(2 > 3 ∨ 4 > 2) ⇔ 5 > 2
 %% Cell type:markdown id: tags:
 Man kann eine Aussage natürlich auch auswerten:
 %% Cell type:code id: tags:
 ``` prob
 not(2>3 or 4>2) ⇔ 5>2
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 2>3 or 4>2
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 not(2>3 or 4>2)
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 5>2
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ### Prioritäten
 * höchste Priorität: ¬
 * danach ∧ , ∨
 * danach ⇒ , ⇔
 %% Cell type:code id: tags:
 ``` prob
 2>0 or 3>4 ⇒ 4>5
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 2>0 or (3>4 ⇒ 4>5)
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 (2>0 or 3>4) ⇒ 4>5
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 (1=1 => 2=2) => 3=1
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 *Achtung:*
 * in Rodin/Event-B haben Konjunktion und Disjunktion die gleiche Priorität und dürfen nicht ohne Klammerung gemischt werden. In klassischem B schon.
 * Das gleiche gilt für => und <=>.
 * In Rodin ist auch keine Assoziativität für => oder <=> definiert worden. Man darf diese Operatoren also auch nicht untereinander ohne Klammern mischen.
 %% Cell type:code id: tags:
 ``` prob
 2>1 or 2>3 & 3>4
 ```
 %% Output
    de.prob.animator.domainobjects.EvaluationException: Could not parse formula:
    Parsing predicate failed because: Operator: ∨ is not compatible with: ∧, parentheses are required
    Operator: ∨ is not compatible with: ∧, parentheses are required
    Parsing expression failed because: Operator: ∨ is not compatible with: ∧, parentheses are required
    Operator: ∨ is not compatible with: ∧, parentheses are required
    Parsing substitution failed because: Unknown operator:  (expected to find an assignment operator)
    Unknown operator:  (expected to find an assignment operator)
    Code: 2>1 or 2>3 & 3>4
    Unicode translation: 2>1 ∨ 2>3 ∧ 3>4
 %% Cell type:markdown id: tags:
 ## Prädikate
 In Event-B gibt es die Aussagen true (⊤) und false (⊥)  (nicht verwechseln mit den Bool'schen Datenwerten TRUE und FALSE). Im klassichen B gibt es diese beiden Aussagen nicht (wobei ProB `btrue` und `bfalse` akzeptiert).
 %% Cell type:code id: tags:
 ``` prob
 true or false
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 ⊤ or ⊥
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 Wahrheitswerte können über Prädikate hergestellt werden:
 * ein n-äres Pradikat bekommt n Datenwerte und bildet diese auf einen Wahrheitswert ab
 Für alle Datentypen gibt es die binären Pradikate = und ≠ (wobei gilt x ≠ y ⇔ ¬(x=y)).
 Für Zahlen gibt es die mathematischen Vergleichsoperatoren. Für Mengen werden noch weitere Prädikate hinzukommen.
 %% Cell type:code id: tags:
 ``` prob
 2 = 3-1
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 3 ≠ 3+1
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 4 >= 2+2
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ## Quantoren
 In B gibt es zwei Quantoren die neue Variablen einführen:
 * den Existenzquantor (mindestens eins)
 - #x.(P) als ASCII
 - ∃x.(P) als Unicode
 * den Allquantor/Universalquantor (alle / jeder)
 - !x.(P => Q) als ASCII
 - ∀(x).(P ⇒ Q) als Unicode
 Der Rumpf eines Allquantors muss also immer eine Implikation auf oberster Ebene verwenden.
 %% Cell type:code id: tags:
 ``` prob
 ∃x .(  x>2 )
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 ∀x .( x>2 ⇒ x>3 )
 ```
 %% Output
    $\mathit{FALSE}$
    **Solution:**
    * $\mathit{x} = 3$
    FALSE
    Solution:
    	x = 3
 %% Cell type:code id: tags:
 ``` prob
 ∀x .( x>2 & x < 100 ⇒  ∃y.(x=y+y))
 ```
 %% Output
    $\mathit{FALSE}$
    **Solution:**
    * $\mathit{x} = 3$
    FALSE
    Solution:
    	x = 3
 %% Cell type:code id: tags:
 ``` prob
 ∀x .( x>2 & x < 100 ⇒  ∃y.(x=y+y) or ∃y.(x=y+y+1))
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ### Typisierung bei Quantoren
 B basiert auf typisierter Logik
 * Bei Quantoren, zum Beispiel, müssen die neuen Variablen typisiert werden
 - ∃x.(2>3)  ist nicht erlaubt
 Generell: für   ∃x.(P)  und  ∀(x).(P ⇒ Q)  muss P den Typen von x bestimmbar machen.
 Deshalb ist der Rumpf eines Allquantors auch immer eine Implikation.
 Beim Existenzquantor wird oft eine Konjunktion verwendet.
 Warum macht eine Implikation beim Existenzquantor fast nie Sinn?
 %% Cell type:code id: tags:
 ``` prob
 ∃x.(x>-100000 => 22=1)
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ## Arithmetik
 B bietet Arithmetik über *ganzen* Zahlen an.
 Folgende Zahlenmengen sind vordefiniert:
 * INT, ℤ
 * NAT = {x|x≥0}, ℕ
 * NAT1= {x|x≥1}, ℕ1
 In Atelier-B (klassisches B für die Softwareentwicklung, nicht in Rodin) wird zwischen mathematischen und implementierbaren Zahlen unterschieden:
 * Mathematische ganze Zahlen: INTEGER, NATURAL, NATURAL1
 * Implementierbare ganze Zahlen: INT, NAT, NAT1
 * MININT, MAXINT
 NATURAL aus dem klassischem B entspricht also NAT in Rodin.
 NAT aus dem klassischen B entspricht 0..MAXINT in Rodin, wobei MAXINT als Konstante definiert werden muss.
 %% Cell type:code id: tags:
 ``` prob
 0:ℕ
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 0:NAT1
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 ### Divsion
 B benutzt ganzzahlige Division und es gilt zB das Gesetz
 *  b≠0 ⇒ a ÷ b = (−a) ÷ (−b)
 Man hat auch:
 %% Cell type:code id: tags:
 ``` prob
 3/2
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 -3 / 2
 ```
 %% Output
    $-1$
    −1
 %% Cell type:markdown id: tags:
 In Python bekommt man
 ```
 >>> (-3)//2
 -2
 ```
 %% Cell type:markdown id: tags:
 Division durch 0 und modulo durch negative Zahlen ist nicht definiert.
 %% Cell type:code id: tags:
 ``` prob
 100 mod -2
 ```
 %% Output
    :eval: NOT-WELL-DEFINED:
    mod not defined for negative numbers: 100 mod-2
 %% Cell type:markdown id: tags:
 ## Mengen
 Mengen sind ein fundamentales Konzept in B.
 In eine Mengen darf man nur Werten eines gleichen Typs packen.
 Mengen dürfen aber verschachtelt werden.
 Die einfachste Menge ist die leere Menge:
 %% Cell type:code id: tags:
 ``` prob
 {}
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:markdown id: tags:
 Man kann Mengen durch **explizite Aufzählung** (Enumeration, set extension auf Englisch) definieren:
 %% Cell type:code id: tags:
 ``` prob
 {1,1+1,2,2+2,3,4}
 ```
 %% Output
    $\{1,2,3,4\}$
    {1,2,3,4}
 %% Cell type:markdown id: tags:
 Mengen können auch mit Hilfe eines Prädikats definiert werden (set comprehension auf Englisch). Die Syntaxform ist `{x | P}`.
 %% Cell type:code id: tags:
 ``` prob
 {x | x>0 & x<5}
 ```
 %% Output
    $\{1,2,3,4\}$
    {1,2,3,4}
 %% Cell type:code id: tags:
 ``` prob
 {x|x>2+2}
 ```
 %% Output
    $\{\mathit{x}\mid\mathit{x} > 4\}$
    {x∣x > 4}
 %% Cell type:markdown id: tags:
 Eine Menge an Zahlen kann auch mit der Intervallnotation ``a..b`` definiert werden:
 %% Cell type:code id: tags:
 ``` prob
 1..4
 ```
 %% Output
    $\{1,2,3,4\}$
    {1,2,3,4}
 %% Cell type:markdown id: tags:
 Die Kardinalität (Mächtigkeit) einer endlichen Menge kann mit dem card Operator bestimmt werden:
 %% Cell type:code id: tags:
 ``` prob
 card({1,1+1,2,2+2,3,4})
 ```
 %% Output
    $4$
    4
 %% Cell type:code id: tags:
 ``` prob
 card({x|x>2})
 ```
 %% Output
-    :eval: NOT-WELL-DEFINED:
+    Error from ProB: NOT-WELL-DEFINED
-    card applied to very large set, cardinality not representable in ProB:  closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(none)]))
+    Error: card applied to infinite set, cardinality not representable in ProB:  {x|x > 2} (:1:0 to 1:13)
+    card({x|x>2})
 %% Cell type:markdown id: tags:
 Mengen können andere Mengen beinhalten:
 %% Cell type:code id: tags:
 ``` prob
 { 1..4 , {1,2,3,4,2+2}, {}}
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1,2,3,4\}\}$
    {∅,{1,2,3,4}}
 %% Cell type:code id: tags:
 ``` prob
 card({ 1..4 , {1,2,3,4,2+2}, {}})
 ```
 %% Output
    $2$
    2
 %% Cell type:markdown id: tags:
 Was ist der Untschied zwischen der leeren Menge ∅ und { ∅ }?
 %% Cell type:code id: tags:
 ``` prob
 ∅ = {∅}
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 card(∅)
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 card({∅})
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 ∅ : {∅}
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 Die Notation `{x | P}` wobei eine Menge per Prädikat definiert wird ist die mächtigste Notation.
 %% Cell type:code id: tags:
 ``` prob
 {x | x>1 & x<1  }
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 {x | x=1 or x=2 }
 ```
 %% Output
    $\{1,2\}$
    {1,2}
 %% Cell type:code id: tags:
 ``` prob
 {x | x>=1 & x<=4 }
 ```
 %% Output
    $\{1,2,3,4\}$
    {1,2,3,4}
 %% Cell type:code id: tags:
 ``` prob
 NAT = {x | x>=0 }
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 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 id: tags:
 ``` prob
 {x.x:1..10|x*x}
 ```
 %% Output
    $\{1,4,9,16,25,36,49,64,81,100\}$
    {1,4,9,16,25,36,49,64,81,100}
 %% Cell type:markdown id: tags:
 ## Prädikate über Mengen
 Es gibt die Standardprädikate der Mathematik:
 * ∈
 * ∉
 * ⊆
 * ⊂
 %% Cell type:code id: tags:
 ``` prob
 :prettyprint not({1,2,3} /<<: {1,2,3})
 ```
 %% Output
    $\neg (\{1,2,3\} \not\subset  \{1,2,3\})$
    ¬({1,2,3} ⊄ {1,2,3})
 %% Cell type:markdown id: tags:
 Zusätzlich hat Event-B das partition Prädikat, welches wir weiter unter erklären.
 %% Cell type:markdown id: tags:
 ## Operatoren über Mengen
 * Vereinigung         \/   ∪
 * Schnittmenge      /\   ∩
 * Differenzmenge    \
 * union(S), inter(S) für Menge von Mengen
 * POW(S) (Potenzmenge: Untermengen von S)
 * POW1(S) (nicht leeren Untermengen von S)
 Übung: diese Operatoren durch comprehension sets definieren
 %% Cell type:code id: tags:
 ``` prob
 a = {1,2,4} & b = {2,3,4} & aub1 = a \/ b &
 aub2 = {x | x:a or x:b}
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{a} = \{1,2,4\}$
    * $\mathit{b} = \{2,3,4\}$
    * $\mathit{aub2} = \{1,2,3,4\}$
    * $\mathit{aub1} = \{1,2,3,4\}$
    TRUE
    Solution:
    	a = {1,2,4}
    	b = {2,3,4}
    	aub2 = {1,2,3,4}
    	aub1 = {1,2,3,4}
 %% Cell type:code id: tags:
 ``` prob
 a = {1,2,4} & b = {2,3,4} & aib1 = a/\b &
 aib2 = {x | x:a & x:b}
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{a} = \{1,2,4\}$
    * $\mathit{b} = \{2,3,4\}$
    * $\mathit{aib2} = \{2,4\}$
    * $\mathit{aib1} = \{2,4\}$
    TRUE
    Solution:
    	a = {1,2,4}
    	b = {2,3,4}
    	aib2 = {2,4}
    	aib1 = {2,4}
 %% Cell type:code id: tags:
 ``` prob
 a = {1,2,4} & b = {2,3,4} & aib1 = a \ b
 & aib2 = {x | x:a & x/:b}
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{a} = \{1,2,4\}$
    * $\mathit{b} = \{2,3,4\}$
    * $\mathit{aib2} = \{1\}$
    * $\mathit{aib1} = \{1\}$
    TRUE
    Solution:
    	a = {1,2,4}
    	b = {2,3,4}
    	aib2 = {1}
    	aib1 = {1}
 %% Cell type:code id: tags:
 ``` prob
 {x.x:1..10|x*x}
 ```
 %% Output
    $\{1,4,9,16,25,36,49,64,81,100\}$
    {1,4,9,16,25,36,49,64,81,100}
 %% Cell type:code id: tags:
 ``` prob
 a = {1,2,4} & b = {2,3,4} & c = {4,6} & abc = union({a,b,c})
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{a} = \{1,2,4\}$
    * $\mathit{b} = \{2,3,4\}$
    * $\mathit{c} = \{4,6\}$
    * $\mathit{abc} = \{1,2,3,4,6\}$
    TRUE
    Solution:
    	a = {1,2,4}
    	b = {2,3,4}
    	c = {4,6}
    	abc = {1,2,3,4,6}
 %% Cell type:code id: tags:
 ``` prob
 POW(1..2)
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$
    {∅,{1},{1,2},{2}}
 %% Cell type:code id: tags:
 ``` prob
 POW(BOOL)
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\}$
    {∅,{FALSE},{FALSE,TRUE},{TRUE}}
 %% Cell type:code id: tags:
 ``` prob
 POW(POW(BOOL))
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\emptyset\},\{\emptyset,\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{TRUE}\}\}\}$
    {∅,{∅},{∅,{FALSE}},{∅,{FALSE,TRUE}},{∅,{TRUE}},{{FALSE}},{∅,{FALSE},{FALSE,TRUE}},{∅,{FALSE},{TRUE}},{{FALSE},{FALSE,TRUE}},{{FALSE},{TRUE}},{∅,{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE}},{∅,{FALSE,TRUE},{TRUE}},{{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE},{TRUE}},{{TRUE}}}
 %% Cell type:code id: tags:
 ``` prob
 card(POW(POW(POW(BOOL))))
 ```
 %% Output
    $65536$
    65536
 %% Cell type:markdown id: tags:
 ## Übung: Send More Money
 Man soll 8 Ziffern finden so dass folgende Summe aufgeht
 |   |   |   |   |   |   |
 |---|---|---|---|---|---|
 |   |   | S | E | N | D |
 |   | + | M | O | R | E |
 | = | M | O | N | E | Y |
 Wir brauchen acht Ziffern:
 %% Cell type:code id: tags:
 ``` prob
 {S,E,N,D,M,O,R,Y}<:0..9
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{R} = 0$
    * $\mathit{S} = 0$
    * $\mathit{D} = 0$
    * $\mathit{E} = 0$
    * $\mathit{Y} = 0$
    * $\mathit{M} = 0$
    * $\mathit{N} = 0$
    * $\mathit{O} = 0$
    TRUE
    Solution:
    	R = 0
    	S = 0
    	D = 0
    	E = 0
    	Y = 0
    	M = 0
    	N = 0
    	O = 0
 %% Cell type:markdown id: tags:
 Diese Ziffern sollen alle unterschiedlich sein:
 %% Cell type:code id: tags:
 ``` prob
 {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{R} = 2$
    * $\mathit{S} = 0$
    * $\mathit{D} = 5$
    * $\mathit{E} = 7$
    * $\mathit{Y} = 1$
    * $\mathit{M} = 4$
    * $\mathit{N} = 6$
    * $\mathit{O} = 3$
    TRUE
    Solution:
    	R = 2
    	S = 0
    	D = 5
    	E = 7
    	Y = 1
    	M = 4
    	N = 6
    	O = 3
 %% Cell type:markdown id: tags:
 Die Ziffern S und M dürfen nicht 0 sein:
 %% Cell type:code id: tags:
 ``` prob
 {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
 S /= 0 & M /= 0
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{R} = 3$
    * $\mathit{S} = 2$
    * $\mathit{D} = 5$
    * $\mathit{E} = 7$
    * $\mathit{Y} = 0$
    * $\mathit{M} = 1$
    * $\mathit{N} = 6$
    * $\mathit{O} = 4$
    TRUE
    Solution:
    	R = 3
    	S = 2
    	D = 5
    	E = 7
    	Y = 0
    	M = 1
    	N = 6
    	O = 4
 %% Cell type:markdown id: tags:
 Und jetzt muss noch die Summe stimmen:
 %% Cell type:code id: tags:
 ``` prob
 {S,E,N,D,M,O,R,Y}<:0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
 S /= 0 & M /= 0 &
 S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E =
 M*10000 + O*1000 + N*100 + E*10 + Y
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{R} = 8$
    * $\mathit{S} = 9$
    * $\mathit{D} = 7$
    * $\mathit{E} = 5$
    * $\mathit{Y} = 2$
    * $\mathit{M} = 1$
    * $\mathit{N} = 6$
    * $\mathit{O} = 0$
    TRUE
    Solution:
    	R = 8
    	S = 9
    	D = 7
    	E = 5
    	Y = 2
    	M = 1
    	N = 6
    	O = 0
 %% Cell type:markdown id: tags:
 Wir können auch die Menge aller Lösungen bestimmen:
 %% Cell type:code id: tags:
 ``` prob
 :table {S|->E|->N|->D|->M|->O|->R|->Y |
  {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
   S /= 0 & M /= 0 &
   S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E
   = M*10000 + O*1000 + N*100 + E*10 + Y }
 ```
 %% Output
    |S|E|N|D|M|O|R|Y|
    |---|---|---|---|---|---|---|---|
    |9|5|6|7|1|0|8|2|
    S	E	N	D	M	O	R	Y
    9	5	6	7	1	0	8	2
 %% Cell type:markdown id: tags:
 ## Das Partition Prädikat
 Dieses Prädikat gibt es nur in Event-B und es ist syntaktischer Zucker für einen grösseren äquivalenten Ausdruck:
 ```
 partition(S,S1,S2,...,Sn)
 ```
 steht für
 ```
   S = S1 \/ S2 \/ ... Sn &
   S1 /\ S2 = {} & ... S1 /\ Sn = {} &
   S2 /\ S3 = {} & ... S2 /\ Sn = {}
   ...
   Sn-1 /\ Sn = {}
   ```
 %% Cell type:code id: tags:
 ``` prob
 :language event_b
 ```
 %% Output
    Changed language for user input to Event-B (forced)
 %% Cell type:code id: tags:
 ``` prob
 partition(1..3,{1},{2},{3})
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 :table {a|->b| partition(1..2,a,b)}
 ```
 %% Output
    |a|b|
    |---|---|
    |∅|{1,2}|
    |{1}|{2}|
    |{1,2}|∅|
    |{2}|{1}|
    a	b
    {}	{1,2}
    {1}	{2}
    {1,2}	{}
    {2}	{1}
 %% Cell type:markdown id: tags:
 ## Neue Basismengen
 Vom Benutzer können in Event-B neue Basismengen eingeführt werden
 * werden in der `sets` Sektion von Kontexten eingeführt
 * jede Benutzermenge ist sein eigener Typ!
 Man darf unterschiedliche Mengen bzw. Elemente aus unterschiedlichen Basismengen nicht mischen.
 Es gibt zwei Möglichkeiten:
 1) Enumerated Set: man gibt explizit alle Elemente der neuen Basismenge an
 S = {a,b,c} in klassischem B oder partition(S,{a},{b},{c}).
 2) Deferred Set: man lässt die Menge für Erweiterungen offen
 In Rodin gibt es zwei Wizards zum einführen von enumerated bzw. deferred "carrier" sets.
 %% Cell type:markdown id: tags:
 ## Typen in B
 * es gibt einen Typ für alle Zahlen: INT (ℤ)
 * es gibt den Typ BOOL für die Bool'schen Werte
 * für jede Basismenge gibt es einen eigenen Typen
 * ist t ein Typ, dann ist POW(t) auch ein Typ
 * nächste Woche werden wir noch ein weitere Typkonstruktion sehen
 Jeder Ausdruck und damit auch jede Variable muss genau einen Typen haben. Die Typen müssen mit den Signaturen der B Operatoren kompatibel sein.
 * man kann explizit Typen angeben, mit einem Prädikat `VARIABLE ∈ TYP`, zum Beispiel: `a∈ℤ`
 * oder auf die Typ-Inferenz von Atelier-B, Rodin, ProB hoffen (Atelier-B am schwächsten; ProB am mächtigsten)
 Beispiele:
 %% Cell type:code id: tags:
 ``` prob
 :type 1
 ```
 %% Output
    INT
 %% Cell type:code id: tags:
 ``` prob
 1 ∈ ℤ
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 :type {1}
 ```
 %% Output
    POW(INT)
 %% Cell type:code id: tags:
 ``` prob
 {1} ∈ POW(INT)
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 NAT : POW(INT)
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 :type {}
 ```
 %% Output
    POW(?)
 %% Cell type:markdown id: tags:
 Are the following two expressions well-typed? What are the type inference rules?
 %% Cell type:code id: tags:
 ``` prob
 1+card({TRUE})
 ```
 %% Output
    $2$
    2
 %% Cell type:code id: tags:
 ``` prob
 {TRUE} ∪ {1}
 ```
 %% Output
    de.prob.exception.CliError: Exception while processing command result
 %% Cell type:markdown id: tags:
 ### Inferenzregeln für Typen
 Folgende Regeln sind relevant um die Typen der beiden Ausdrücke oben zu prüfen:
 * type(1) = INTEGER
 * type(TRUE) = BOOL
 * type({ x }) = POW(XT)  where type(x) = XT
 * type(a+b) = INTEGER if type(a)=type(b)=INTEGER
 * type(a ∪ b) = POW(T)  if type(a) = type(b) = POW(T)
 %% Cell type:markdown id: tags:
 # Kleine Beispiele
 %% Cell type:code id: tags:
 ``` prob
 1+x=3
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{x} = 2$
    TRUE
    Solution:
    	x = 2
 %% Cell type:code id: tags:
 ``` prob
 :language event_b
 ```
 %% Output
    Changed language for user input to Event-B (forced)
 %% Cell type:markdown id: tags:
 Wenn man die Menge der Primzahlen so definiert, behält ProB diese als symbolische Menge:
 %% Cell type:code id: tags:
 ``` prob
 Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
 ```
 %% Output
    $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
    **Solution:**
    * $\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)\}$
    TRUE
    Solution:
    	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 %% Cell type:markdown id: tags:
 Man kann aber zum Beispiel eine Primzahl generieren:
 %% Cell type:code id: tags:
 ``` prob
 x∈Primzahlen ∧ Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
 ```
 %% Output
    $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
    **Solution:**
    * $\mathit{x} = 2$
    * $\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)\}$
    TRUE
    Solution:
    	x = 2
    	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 %% Cell type:markdown id: tags:
 Man kann die Menge der Primzahlen auch mit 1..100 schneiden um die Primzahlen bis 100 zu bekommen:
 %% Cell type:code id: tags:
 ``` prob
 Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧
 res = Primzahlen ∩ 1..100
 ```
 %% Output
    $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
    **Solution:**
    * $\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\}$
    * $\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)\}$
    TRUE
    Solution:
    	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}
    	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 %% Cell type:markdown id: tags:
 Hier rechnen wir jetzt die Anzahl der Primzahle bis 1000 aus:
 %% Cell type:code id: tags:
 ``` prob
 Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧
 res = card(Primzahlen ∩ 1..1000)
 ```
 %% Output
    $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
    **Solution:**
    * $\mathit{res} = 168$
    * $\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)\}$
    TRUE
    Solution:
    	res = 168
    	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 %% Cell type:code id: tags:
 ``` prob
 :table {x|x:1..20 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
 ```
 %% Output
    |x|
    |---|
    |1|
    |2|
    |3|
    |5|
    |7|
    |11|
    |13|
    |17|
    |19|
    x
    1
    2
    3
    5
    7
    11
    13
    17
    19
 %% Cell type:code id: tags:
 ``` prob
 ```