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

add presentation

parent 85ce492c
No related branches found
No related tags found
No related merge requests found
Pipeline #99406 passed
%% Cell type:markdown id: tags:
# ProB for Teaching Theoretical Computer Science and Formal Methods
### David Geleßus, Michael Leuschel
### FMTea 2022
https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel
![ProB](./img/prob_logo.png)
%% Cell type:markdown id: tags:
# Intro: Notebooks, Jupyter
%% Cell type:markdown id: tags:
## What is a Notebook?
* Document containing text and executable code blocks
* Code can be executed interactively
* Results are shown in the notebook below the corresponding code
* Similar to a REPL (read-eval-print-loop), with some differences:
* Code blocks can be edited and executed out-of-order
* Results can contain rich text and graphics
* Can be shared with other users
%% Cell type:markdown id: tags:
## Jupyter Notebook
* Browser-based notebook interface
* Open-source and cross-platform
* Originated in the Python community, implemented in Python
* Also supports languages other than
* Language integration provided by a separate *kernel*
%% Cell type:markdown id: tags:
## ProB Jupyter Kernel (https://prob.hhu.de/w/)
* Understands both classical B syntax and Rodin Event-B syntax
* Many features: Code completion, graph visualisation, ...
%% Cell type:markdown id: tags:
# Some Features
%% Cell type:markdown id: tags:
## Evaluating Formulas
Evaluating B expressions and solving predicates:
%% Cell type:code id: tags:
``` prob
1+2
```
%% Output
$3$
3
%% 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
1..5 \/ {-3, 4, 10, 18}
```
%% Output
$\{-3,1,2,3,4,5,10,18\}$
{−3,1,2,3,4,5,10,18}
%% Cell type:markdown id: tags:
Example: Set of all prime numbers < 500
%% Cell type:code id: tags:
``` prob
{x | x > 1 & x < 500 & not(#y.(y > 1 & y < x & x mod y = 0))}
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}/*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \lnot(\exists\mathit{y}\qdot(\mathit{y} > 1 \land \mathit{y} < \mathit{x} \land \mathit{x} \mathit{mod} \mathit{y} = 0))\}$
/*@symbolic*/ {x∣x > 1 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))}
%% Cell type:markdown id: tags:
Outputs are rendered as $\LaTeX$ formulas:
%% Cell type:code id: tags:
``` prob
:prettyprint x > 1 & x < 500 & not(#y.(y > 1 & y < x & x mod y = 0))
```
%% Output
$\mathit{x} > 1 \wedge \mathit{x} < 500 \wedge \neg (\exists \mathit{y}\cdot (\mathit{y} > 1 \wedge \mathit{y} < \mathit{x} \wedge \mathit{x} \mod \mathit{y} = 0))$
x > 1 ∧ x < 500 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))
%% Cell type:markdown id: tags:
Unicode symbols can also be used in inputs:
%% Cell type:code id: tags:
``` prob
{x | x>1 ∧ x<500 ∧ ¬(∃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,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499\}$
{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,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421,431,433,439,443,449,457,461,463,467,479,487,491,499}
%% Cell type:markdown id: tags:
Convenient multiline input, with syntax highlighting and code completion:
%% 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:
Find distinct digits such that this multiplication becomes true:
![ProB](./img/KissKissPassion.png)
(This is a more difficult version of the Send+More=Money puzzle.)
%% Cell type:code id: tags:
``` prob
:table {K,I,S,P,A,O,N | {K,P} ⊆ 1..9 ∧
{I,S,A,O,N} ⊆ 0..9 ∧
(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S)
= 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N ∧
card({K, I, S, P, A, O, N}) = 7}
```
%% Output
|K|I|S|P|A|O|N|
|---|---|---|---|---|---|---|
|2|0|3|4|1|8|9|
K I S P A O N
2 0 3 4 1 8 9
%% Cell type:markdown id: tags:
## Visualisation
In B, sequences are also functions, functions are relations, and relations are sets.
Relations can be displayed visually:
%% Cell type:code id: tags:
``` prob
{x,y | x:1..5 & y:1..5 & x>y}
```
%% Output
$\{(2\mapsto 1),(3\mapsto 1),(3\mapsto 2),(4\mapsto 1),(4\mapsto 2),(4\mapsto 3),(5\mapsto 1),(5\mapsto 2),(5\mapsto 3),(5\mapsto 4)\}$
{(2↦1),(3↦1),(3↦2),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(5↦4)}
%% 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:
# Applications
%% Cell type:markdown id: tags:
* Interactive Development
* Documentation of Models
* Documentation of ProB's standard libraries
%% Cell type:markdown id: tags:
## Use in Teaching
* Course materials/lecture notes as notebooks
* Students can execute examples themselves and experiment with the code
* Visualisation of relations, graphs, etc.
* `nbconvert` renders notebooks to HTML, PDF, etc.
* Exercise sheets as notebooks
* An incomplete notebook with exercises is provided
* Students solve the exercises and turn in the finished notebook
* `nbgrader` assists with creating and grading exercises
* Automatic grading sometimes possible
%% Cell type:markdown id: tags:
## Example: Course Notes for Theoretical CS (German)
%% Cell type:markdown id: tags:
### DFA
Ein __deterministischer endlicher Automat__ (kurz DFA für
deterministic finite automaton) ist ein Quintupel
$M =(\Sigma, Z, \delta , z_0, F)$, wobei
* $\Sigma$ ein Alphabet ist,
* $Z$ eine endliche Menge von Zuständen mit
$\Sigma \cap Z = \emptyset$,
* $\delta : Z \times \Sigma \rightarrow Z$ die Überführungsfunktion,
* $z_0 \in Z$ der Startzustand und
* $F \subseteq Z$ die Menge der Endzustände (Finalzustände).
%% Cell type:code id: tags:
``` prob
MACHINE DFA
SETS
Z = {z0,z1,z2,z3}
CONSTANTS Σ, F, δ
PROPERTIES
F ⊆ Z ∧
δ ∈ (Z×Σ) → Z
/* Der Automat von Folie 10: */
Σ = {0,1} ∧
F = {z2} ∧
δ = { (z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 }
DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{a,b|(a,0)|->b:δ});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0}) // Kante für den Startknoten
END
```
%% Output
Loaded machine: DFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Executed operation: SETUP_CONSTANTS()
%% Cell type:markdown id: tags:
Ein Automat befindet sich jeweils in einem der Zustände aus Z. Am Anfang befindet er sich in $z_0$.
Der Automat kann jeweils in einem Zustand $z$ ein Symbol $x$ aus $\Sigma$ verarbeiten und wechselt dann in den Zustand $\delta(z,x)$.
Zum Beispiel, wenn der DFA im Startzustand z0 das Symbol $0$ erhält wechselt er nach:
%% Cell type:code id: tags:
``` prob
δ(z0,0)
```
%% Output
$\mathit{z1}$
z1
%% Cell type:markdown id: tags:
Wenn der Automat dann das Symbol 1 erhält wechselt er von Zustand $z1$ nach:
%% Cell type:code id: tags:
``` prob
δ(z1,1)
```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags:
Da $z2\in F$ ein Endzustand ist, akzeptiert der DFA das Wort $01$ (oder $[0,1]$ in der Notation vom Notebook).
### Arbeitsweise eines DFAs
Ein DFA $M= (\Sigma, Z, \delta , z_0, F)$ akzeptiert bzw. verwirft eine
Eingabe $x$ wie folgt:
* $M$ beginnt beim Anfangszustand $z_0$ und führt insgesamt $|x|$ Schritte aus.
* Der Lesekopf wandert dabei v.l.n.r. über das Eingabewort $x$, Symbol
für Symbol, und ändert dabei seinen Zustand jeweils gemäß der
Überführungsfunktion $\delta$:
Ist $M$ im Zustand $z \in Z$ und liest das
Symbol $a \in \Sigma$ und gilt $\delta(z,a) = z'$, so ändert $M$ seinen
Zustand in $z'$.
* Ist der letzte erreichte Zustand (nachdem $x$ abgearbeitet ist)
* ein Endzustand, so akzeptiert $M$ die Eingabe $x$;
* andernfalls lehnt $M$ sie ab.
![Arbeitsweise](./img/endl_auto.png)
%% Cell type:markdown id: tags:
Da in diesem Automaten z0 kein Endzustand ist, wird zum Beispiel das leere Wort abgelehnt:
%% Cell type:code id: tags:
``` prob
z0 ∈ F
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
#### Zustandgraph
Man kann den DFA auch grafisch darstellen: Endzustände sind mit einem doppelten Kreis gekennzeichnet, der Anfangszustand wird durch eine besondere Startkante gekennzeichnet.
Formal ist dies so definiert:
Ein DFA $M= (\Sigma, Z, \delta , z_0, F)$ lässt sich anschaulich durch
seinen __Zustandsgraphen__ darstellen,
* dessen Knoten die Zustände von $M$ und
* dessen Kanten Zustandsübergänge gemäß der
Überführungsfunktion $\delta$ repräsentieren.
* Gilt $\delta(z,a) = z'$ für ein Symbol $a \in \Sigma$ und für
zwei Zustände $z, z' \in Z$, so hat dieser Graph eine gerichtete
Kante von $z$ nach $z'$, die mit $a$ beschriftet ist.
* Der Startzustand wird durch einen Pfeil auf $z_0$ dargestellt.
* Endzustände sind durch einen Doppelkreis markiert.
Für den Automaten oben ergiebt dies folgenden Zustandsgraphen.
(Anmerkung: diese Darstellung erfordert eine neue Version des ProB-Jupyter-Kernels. Falls diese bei ihnen nicht funktioniert schauen Sie sich die Abbildung auf den Folien an).
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
# Conclusion
* ProB Jupyter notebooks allow conveniently working interactively with B
* Usable standalone or with existing models
* Applications: development, documentation, teaching
* Jupyter Notebook makes it easy to integrate new languages/tools in notebooks
* The Jupyter ecosystem provides a standard file format and useful tools (`nbconvert`, `nbgrader`, ...)
%% Cell type:markdown id: tags:
### Links
Load this notebook in your browser: https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob2-jupyter-kernel.git/master?filepath=notebooks%2Fpresentations%2FABZ%202021.ipynb
Download and install locally: https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment