Skip to content
Snippets Groups Projects
Commit 8014ecdd authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add Bad Honnef presentation

parent fbe232dd
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/presentations/BadHonnef_2019.ipynb 0 → 100644
+ 1007
− 0
View file @ 8014ecdd
%% Cell type:markdown id: tags:
# Ein Jupyter-Kernel für Logik und Mengentheorie
### David Geleßus, Michael Leuschel
### Bad Honnef, 2019
%% Cell type:markdown id: tags:
# Einführung: Notebooks, Jupyter
%% Cell type:markdown id: tags:
## Was ist ein Notebook?
* Dokument mit Text und ausführbaren Code-Abschnitten
* Code kann interaktiv ausgeführt werden
* Ergebnisse erscheinen im Notebook unter dem jeweiligem Code
* Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden:
* Code-Abschnitte können "außer der Reihe" bearbeitet und ausgeführt werden
* Ausgaben können formatierten Text und Grafiken enthalten
* Speicherbar als Datei
* Code kann später neu ausgeführt werden
* Weitergabe an andere Nutzer möglich
* Implementierungen: Mathematica, Maple, Jupyter, u. a.
%% Cell type:markdown id: tags:
## Jupyter Notebook
* Browserbasierte Notebook-Oberfläche
* Open Source und plattformübergreifend
* Stammt aus der Python-Community, in Python implementiert
* Jupyter-Notebooks können aber verschiedene Programmiersprachen verwenden
* Dazu trennt Jupyter strikt zwischen Frontend und Kernel:
* Das allgemeine **Frontend** implementiert z. B. Benutzeroberfläche und Dateiformat
* Ein sprachspezifischer **Kernel** stellt die Sprache dem Frontend zur Verfügung
* Schnittstellen zwischen Frontend und Kernel sind sprachneutral
* Kernel können in (fast) jeder Sprache implementiert werden, kein Python-Code nötig
%% Cell type:markdown id: tags:
## ProB
* Werkzeug zur Animation, Verifikation und Visualisierung formeller Spezifikationen
* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.
* Unterstützt hauptsächlich B-Spezifikationen (klassisches B, Event-B)
* Versteht auch andere Sprachen wie TLA<sup>+</sup> und CSP<sub>M</sub>
* ProBs APIs sind für alle Sprachen gleich
* Der ProB 2-Jupyter-Kernel unterstützt daher (fast) alle Sprachen, die ProB versteht
%% Cell type:markdown id: tags:
## Architektur von ProB
* **`probcli`:** Kern/Hauptteil von ProB
* Implementiert in SICStus Prolog
* Erlaubt Animation, Visualisierung, Verifikation von formellen Spezifikationen
* Unterstützt u. A. (klassisches) B, Event-B, TLA<sup>+</sup>, CSP<sub>M</sub>
* Kommandozeilentool oder interaktive REPL
* **ProB 2-Java-API:** (aka ProB 2-Kernel; ≠ ProB 2-Jupyter-Kernel!)
* Objektorientierte Java-Schnittstelle für ProB
* Verwaltet automatisch eine oder mehrere `probcli`-Instanzen
* **ProB 2-Jupyter-Kernel:** Jupyter-Kernel-Implementierung für ProB
* In Java implementiert
* Ansteuerung von ProB durch ProB 2-Java-API
* Kommunikation mit Jupyter durch Jupyter-JVM-BaseKernel
%% Cell type:markdown id: tags:
## Formeln auswerten
* B-Ausdrücke auswerten und Prädikate lösen wie in `probcli -repl`
Zum Beispiel, Primzahlen bis 50 ausgeben:
%% Cell type:code id: tags:
``` prob
{x | x > 1 & x < 50 & not(#y.(y > 1 & y < x & x mod y = 0))}
```
%% Output
$\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47\}$
{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47}
%% Cell type:code id: tags:
``` prob
:prettyprint x > 1 & x < 50 & not(#y.(y > 1 & y < x & x mod y = 0))
```
%% Output
$\mathit{x} > 1 \wedge \mathit{x} < 50 \wedge \neg (\exists \mathit{y}\cdot (\mathit{y} > 1 \wedge \mathit{y} < \mathit{x} \wedge \mathit{x} \mod \mathit{y} = 0))$
x > 1 ∧ x < 50 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))
%% Cell type:markdown id: tags:
Eingabe als Unicode ist auch erlaubt:
%% Cell type:code id: tags:
``` prob
{x | x>1 ∧ x<50 ∧ ¬(∃y.(y>1 ∧ y<x ∧ x mod y=0))}
```
%% Output
$\{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47\}$
{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47}
%% Cell type:markdown id: tags:
Mehrzeilige Eingabe ist möglich, es gibt Syntax-Highlighting und Code Completion.
%% Cell type:code id: tags:
``` prob
{S, E, N, D, M, O, R, Y} <: 0..9
& S > 0 & M > 0
& card({S, E, N, D, M, O, R, Y}) = 8
&
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:
Mithilfe der Mengentheorie kann man alle Lösungen finden, und mit dem ```:table``` Kommando als Tabelle ausgeben.
%% 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
& S > 0 & M > 0 // <--
& card({S, E, N, D, M, O, R, Y}) = 8
&
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:
In B sind Folgen auch Funktionen, Funktionen auch Relationen, Relationen auch Mengen.
Relationen können in Jupyter auch grafisch dargestellt werden.
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("k5",{x,y|x:1..5 & y:1..5 & x>y})
```
%% Output
<Dot visualization: expr_as_graph [("k5",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:code id: tags:
``` prob
:pref DOT_ENGINE=circo
```
%% Output
Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("k5",{x,y|x:1..5 & y:1..5 & x>y})
```
%% Output
<Dot visualization: expr_as_graph [("k5",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:markdown id: tags:
# Anwendungsmöglichkeiten
%% Cell type:markdown id: tags:
## Interaktive Nutzung als REPL
* Jupyter Notebook kann wie eine REPL benutzt werden
* Vorteile: mehrzeilige Eingaben, formatierte Ausgaben, verbesserte Editor-Funktionen, speicherbar
* Alternative: `jupyter console` ermöglicht Verwendung von Jupyter-Kerneln im Terminal
* Verhält sich wie eine klassische REPL, arbeitet nicht mit Notebooks
* Unterstützt trotzdem erweiterte Funktionen: Eingabeverlauf, Code-Vervollständigung
%% Cell type:markdown id: tags:
## Interaktive Experimentierung
* Beliebige Stellen im Notebook können bearbeitet und neu ausgeführt werden
* Vereinfacht Testen von Änderungen am Code, z. B.:
* Andere Konstanten-/Präferenzwerte
* Hinzufügen/Entfernen von Invarianten/Guards
* Ändern der Operationsfolge
* Auch Notebooks von anderen Nutzern können ohne Weiteres bearbeitet werden
* Notebook-Dateien sind nie "schreibgeschützt"
* Anzeige und Bearbeitung nutzen die gleiche Oberfläche
* Anwendungen:
* ProB-Notebook als Dokumentation und Beispielcode zu einem B-Modell
* ProB-Notebook
* Übungsblätter für Lehrveranstaltungen (B, Logik, Mengentheorie, theoretische Informatik) als Notebooks
%% Cell type:markdown id: tags:
# Anwendung als Dokumentation (Bibliothek von ProB)
## LibraryRegex
This library provides various facilities for pattern matching with regular expressions.
You can obtain the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "LibraryRegex.def"`
The file `LibraryRegex.def` is also bundled with ProB and can be found in the `stdlib` folder (as of version 1.8.3-beta4).
%% Cell type:code id: tags:
``` prob
::load
MACHINE Jupyter_LibraryRegex
DEFINITIONS "LibraryRegex.def"; "LibraryStrings.def"
END
```
%% Output
Loaded machine: Jupyter_LibraryRegex
%% Cell type:markdown id: tags:
### REGEX_SEARCH_ALL
This external function searches for **all** occurences of a pattern in a string and returns the matched strings as a B sequence.
It always starts to match at the beginning.
Type: $STRING \times STRING \rightarrow seq(STRING)$.
%% Cell type:code id: tags:
``` prob
REGEX_SEARCH_ALL("abcdef000234daf567","([1-9])([0-9]*)")
```
%% Output
$\{(1\mapsto\text{"234"}),(2\mapsto\text{"567"})\}$
{(1↦"234"),(2↦"567")}
%% Cell type:code id: tags:
``` prob
REGEX_SEARCH_ALL("abc-äéà-123","[[:alpha:]]")
```
%% Output
$[\text{"a"},\text{"b"},\text{"c"},\text{"ä"},\text{"é"},\text{"à"}]$
["a","b","c","ä","é","à"]
%% Cell type:markdown id: tags:
# Anwendung: Interaktive Skripte
%% Cell type:code id: tags:
``` prob
::load
MACHINE BaseTypes
SETS PERSONS = {peter,paul,mary}; COLOURS = {red,green,blue}
END
```
%% Cell type:markdown id: tags:
In mathematics a binary relation over the sets $A$ and $B$ is defined to be
a subset of $A\times B$.
The Cartesian product $A \times B$ in turn is defined to be the set of pairs
$a \mapsto b$ such that $a\in A$ and $b\in B$.
For example, we have:
%% Cell type:code id: tags:
``` prob
PERSONS × COLOURS
```
%% Output
$\{(\mathit{peter}\mapsto \mathit{red}),(\mathit{peter}\mapsto \mathit{green}),(\mathit{peter}\mapsto \mathit{blue}),(\mathit{paul}\mapsto \mathit{red}),(\mathit{paul}\mapsto \mathit{green}),(\mathit{paul}\mapsto \mathit{blue}),(\mathit{mary}\mapsto \mathit{red}),(\mathit{mary}\mapsto \mathit{green}),(\mathit{mary}\mapsto \mathit{blue})\}$
{(peter↦red),(peter↦green),(peter↦blue),(paul↦red),(paul↦green),(paul↦blue),(mary↦red),(mary↦green),(mary↦blue)}
%% Cell type:markdown id: tags:
A particular relation could be the following one, which is a subset of PERSONS × COLOURS:
%% Cell type:code id: tags:
``` prob
{peter|->green,peter|->blue,mary|->blue}
```
%% Output
$\{(\mathit{peter}\mapsto \mathit{green}),(\mathit{peter}\mapsto \mathit{blue}),(\mathit{mary}\mapsto \mathit{blue})\}$
{(peter↦green),(peter↦blue),(mary↦blue)}
%% Cell type:markdown id: tags:
We can visualize this relation graphically as follows:
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("r1",{peter|->green,peter|->blue,mary|->blue})
```
%% Output
<Dot visualization: expr_as_graph [("r1",{(peter,green),(peter,blue),(mary,blue)})]>
%% Cell type:code id: tags:
``` prob
:table {peter|->green,peter|->blue,mary|->blue}
```
%% Output
|prj1|prj2|
|---|---|
|$\mathit{peter}$|$\mathit{green}$|
|$\mathit{peter}$|$\mathit{blue}$|
|$\mathit{mary}$|$\mathit{blue}$|
prj1 prj2
peter green
peter blue
mary blue
%% Cell type:markdown id: tags:
As in B a relation is a set of pairs, all set operators can be applied to relations.
For example,
%% Cell type:code id: tags:
``` prob
{peter|->green,peter|->blue,mary|->blue} - {mary|->blue}
```
%% Output
$\{(\mathit{peter}\mapsto \mathit{green}),(\mathit{peter}\mapsto \mathit{blue})\}$
{(peter↦green),(peter↦blue)}
%% Cell type:code id: tags:
``` prob
{peter|->green,peter|->blue,mary|->blue} /\ {mary}*COLOURS
```
%% Output
$\{(\mathit{mary}\mapsto \mathit{blue})\}$
{(mary↦blue)}
%% Cell type:code id: tags:
``` prob
```
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment