Skip to content
Snippets Groups Projects
Commit 22a7f683 authored by dgelessus's avatar dgelessus
Browse files

Update ABZ 2021 slides again

parent 9b059dd9
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/presentations/ABZ 2021.ipynb
+ 63
− 17
View file @ 22a7f683
%% 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
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
$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
$\{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
$\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:
## 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:
## 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
Loaded machine: Lift
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
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
$1$
1
%% Cell type:code id: tags:
``` prob
:exec up
```
%% Output
Executed operation: up()
%% Cell type:code id: tags:
``` prob
curfloor
```
%% Output
$2$
2
%% Cell type:code id: tags:
``` prob
:modelcheck
```
%% Output
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
* -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
<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
* 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
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
$3$
3
%% Cell type:code id: tags:
``` prob
STRING_LENGTH("")
```
%% Output
$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
$\{(1\mapsto\text{"filename"}),(2\mapsto\text{"ext"})\}$
{(1↦"filename"),(2↦"ext")}
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("filename.ext","/")
```
%% Output
$\{(1\mapsto\text{"filename.ext"})\}$
{(1↦"filename.ext")}
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("usr/local/lib","/")
```
%% Output
$\{(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
* `nbconvert` renders notebooks to standard formats (HTML, PDF)
* `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
* 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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment