Skip to content
GitLab
Commit 2b50c3c7 authored by dgelessus's avatar dgelessus
Browse files

Shorten ABZ 2021 slides slightly

parent 22a7f683
Pipeline #63159 passed with stage
in 6 minutes and 37 seconds
Hide whitespace changes
Inline Side-by-side
notebooks/presentations/ABZ 2021.ipynb
View file @ 2b50c3c7
......@@ -672,7 +672,7 @@
{
"data": {
"text/plain": [
"0.040 sec, 7 of 7 states processed, 11 transitions"
"0.037 sec, 7 of 7 states processed, 11 transitions"
]
},
"metadata": {},
......@@ -908,21 +908,7 @@
}
},
"source": [
"## Interactive Usage as a REPL\n",
"\n",
"* Jupyter Notebook can be used like a REPL\n",
"* Advantages: easy multi-line input, rich text output, advanced editor features, saveable"
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"## Interactive Editing of Models\n",
"## Interactive Development\n",
"\n",
"* Any part of a notebook can be edited and re-executed\n",
"* Simplifies testing changes to the code, e.g.:\n",
......@@ -1161,7 +1147,7 @@
"\n",
"* Course materials/lecture notes as notebooks\n",
" * Students can execute examples themselves and experiment with the code\n",
" * Visualisation of concepts like relations, finite automata\n",
" * Visualisation of relations, graphs, etc.\n",
" * `nbconvert` renders notebooks to HTML, PDF, etc.\n",
"* Exercise sheets as notebooks\n",
" * An incomplete notebook with exercises is provided\n",
......@@ -1542,7 +1528,6 @@
"* ProB Jupyter notebooks allow conveniently working interactively with B\n",
"* Usable standalone or with existing models\n",
"* Applications: development, documentation, teaching\n",
"* Also has uses outside of formal methods, e.g. teaching theoretical CS\n",
"* Jupyter Notebook makes it easy to integrate new languages/tools in notebooks\n",
"* The Jupyter ecosystem provides a standard file format and useful tools (`nbconvert`, `nbgrader`, ...)"
]
......
%% Cell type:markdown id: tags:
# ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods
### David Geleßus, Michael Leuschel
### ABZ 2021
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
* Notebooks are saved as a file
* Code can be re-executed later
* Can be shared with other users
* Implementations: Mathematica, Maple, Jupyter, others
%% 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 Python
* Language integration provided by a separate *kernel*
* Kernels: Python, Julia, Java, B, others
%% Cell type:markdown id: tags:
## ProB (https://prob.hhu.de/w/)
* Animation, verification and visualisation tool for formal specifications
* Based on a solver for predicate logic, arithmetic, set theory
* Supports mainly B specifications (classical B, Event-B)
* Also understands some other formalisms, e.g. TLA<sup>+</sup> and Z
%% Cell type:markdown id: tags:
# Features
%% Cell type:markdown id: tags:
## Evaluating Formulas
Evaluating B expressions and solving predicates:
%% Cell type:code id: tags:
``` prob
1 + 2
```
%%%% Output: execute_result
$3$
3
%% Cell type:code id: tags:
``` prob
1 + x = 3
```
%%%% Output: execute_result
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = 2$
TRUE
Solution:
x = 2
%% Cell type:code id: tags:
``` prob
1..5 \/ {-3, 4, 10, 18}
```
%%%% Output: execute_result
$\{-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: execute_result
$\{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:
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: execute_result
$\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: execute_result
$\{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: execute_result
|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:
## 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: execute_result
$\{(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: execute_result
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: execute_result
<Dot visualization: expr_as_graph [("K5",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:markdown id: tags:
## Working with Machines
%% Cell type:code id: tags:
``` prob
MACHINE Lift
VARIABLES curfloor
INVARIANT curfloor : 1..5
INITIALISATION curfloor := 1
OPERATIONS
up = PRE curfloor <= 5 THEN curfloor := curfloor + 1 END;
down = PRE curfloor > 1 THEN curfloor := curfloor - 1 END
END
```
%%%% Output: execute_result
Loaded machine: Lift
%% Cell type:code id: tags:
``` prob
:init
```
%%%% Output: execute_result
Executed operation: INITIALISATION()
%% Cell type:markdown id: tags:
Expressions are evaluated in the current state of the machine.
%% Cell type:code id: tags:
``` prob
curfloor
```
%%%% Output: execute_result
$1$
1
%% Cell type:code id: tags:
``` prob
:exec up
```
%%%% Output: execute_result
Executed operation: up()
%% Cell type:code id: tags:
``` prob
curfloor
```
%%%% Output: execute_result
$2$
2
%% Cell type:code id: tags:
``` prob
:modelcheck
```
%%%% Output: display_data
%%%% Output: execute_result
Model check uncovered an error: Invariant violation found.
Use :trace to view the trace to the error state.
%% Cell type:code id: tags:
``` prob
:trace
```
%%%% Output: execute_result
* -1: Root state
* 0: `INITIALISATION()`
* 1: `up()`
* 2: `up()`
* 3: `up()`
* 4: `up()`
* 5: `up()` **(current)**
-1: Root state
0: INITIALISATION()
1: up()
2: up()
3: up()
4: up()
5: up() (current)
%% Cell type:code id: tags:
``` prob
:dot state_space
```
%%%% Output: execute_result
<Dot visualization: state_space []>
%% Cell type:markdown id: tags:
# Applications
%% Cell type:markdown id: tags:
## Interactive Usage as a REPL
* Jupyter Notebook can be used like a REPL
* Advantages: easy multi-line input, rich text output, advanced editor features, saveable
%% Cell type:markdown id: tags:
## Interactive Editing of Models
## Interactive Development
* Any part of a notebook can be edited and re-executed
* Simplifies testing changes to the code, e.g.:
* Changing the values of constants and preferences
* Adding/modifying/removing invariants/guards
* Notebooks created by other users can be easily edited
* Notebook files are never "read-only"
* The same interface is used for viewing and editing notebooks
%% Cell type:markdown id: tags:
## Documentation of Models
* Notebooks can load existing models from files
* Animation steps can be used to demonstrate behavior of model in specific cases
* Similar to trace files, but with ability to add inline explanations
* Visualisation features make states easier to understand
%% Cell type:markdown id: tags:
## Example: Documentation of ProB Standard Libraries
%% Cell type:markdown id: tags:
# External Functions
## LibraryStrings
In pure B there are only two built-in operators on strings: equality $=$ and inequality $\neq$.
This library provides several string manipulation functions, and assumes that STRINGS are
sequences of unicode characters (in UTF-8 encoding).
You can obtain the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "LibraryStrings.def"`
The file `LibraryStrings.def` is bundled with ProB and can be found in the `stdlib` folder.
You can also include the machine `LibraryStrings.mch` instead of the definition file;
the machine defines some of the functions below as proper B functions (i.e., functions
for which you can compute the domain and use constructs such as
relational image).
%% Cell type:code id: tags:
``` prob
MACHINE Jupyter_LibraryStrings
DEFINITIONS "LibraryStrings.def"
END
```
%%%% Output: execute_result
Loaded machine: Jupyter_LibraryStrings
%% Cell type:markdown id: tags:
### STRING_LENGTH
This external function takes a string and returns the length.
Type: $STRING \rightarrow INTEGER$.
%% Cell type:code id: tags:
``` prob
STRING_LENGTH("abc")
```
%%%% Output: execute_result
$3$
3
%% Cell type:code id: tags:
``` prob
STRING_LENGTH("")
```
%%%% Output: execute_result
$0$
0
%% Cell type:markdown id: tags:
### STRING_SPLIT
This external function takes two strings and separates the first string
according to the separator specified by the second string.
Type: $STRING \times STRING \rightarrow \mathit{seq}(STRING) $.
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("filename.ext",".")
```
%%%% Output: execute_result
$\{(1\mapsto\text{"filename"}),(2\mapsto\text{"ext"})\}$
{(1↦"filename"),(2↦"ext")}
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("filename.ext","/")
```
%%%% Output: execute_result
$\{(1\mapsto\text{"filename.ext"})\}$
{(1↦"filename.ext")}
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("usr/local/lib","/")
```
%%%% Output: execute_result
$\{(1\mapsto\text{"usr"}),(2\mapsto\text{"local"}),(3\mapsto\text{"lib"})\}$
{(1↦"usr"),(2↦"local"),(3↦"lib")}
%% 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 concepts like relations, finite automata
* 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: execute_result
Loaded machine: DFA
%% Cell type:code id: tags:
``` prob
:constants
```
%%%% Output: execute_result
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: execute_result
$\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: execute_result
$\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: execute_result
$\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: execute_result
<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
* Also has uses outside of formal methods, e.g. teaching theoretical CS
* 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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment