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

Add initial version of ABZ 2021 slides

parent 80631d19
No related branches found
No related tags found
No related merge requests found
%% 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
* Jupyter notebooks can also use languages other than Python
* Strict separation between frontend and kernel:
* The generic **frontend** implements e.g. the user interface and file format
* A language-specific **kernel** allows the frontend to use the language
* Language-neutral interface between frontend and kernel
* Kernels can be implemented in (nearly) any language - no Python code necessary
%% 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, set theory with relations, functions, and arithmetic
* Supports mainly B specifications (classical B, Event-B)
* Also understands some other formalisms, e.g. TLA<sup>+</sup> and Z
* Core of ProB implemented in SICStus Prolog
* High-level Java API available
* Jupyter kernel written in Java based on this API
%% 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 \/ 10..15
```
%% Output
$\{1,2,3,4,5,10,11,12,13,14,15\}$
{1,2,3,4,5,10,11,12,13,14,15}
%% 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
{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:
Finding all solutions as a set and displaying them as a table using the `:table` command:
%% 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 := 5
OPERATIONS
up = PRE curfloor < 5 THEN curfloor := curfloor + 1 END;
down = BEGIN 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
$5$
5
%% Cell type:code id: tags:
``` prob
:exec down
```
%% Output
Executed operation: down()
%% Cell type:code id: tags:
``` prob
curfloor
```
%% Output
$4$
4
%% 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: `down()`
* 2: `down()`
* 3: `down()`
* 4: `down()`
* 5: `down()` **(current)**
-1: Root state
0: INITIALISATION()
1: down()
2: down()
3: down()
4: down()
5: down() (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/removing invariants/guards
* Changing the order of operations
* 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 be used to document an existing model
* 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:code id: tags:
``` prob
STRING_SPLIT("",".")
```
%% Output
$\{(1\mapsto\text{""})\}$
{(1↦"")}
%% 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)
* 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
%% Cell type:code id: tags:
``` prob
MACHINE BaseTypes
SETS PERSONS = {peter,paul,mary}; COLOURS = {red,green,blue}
END
```
%% Output
Loaded machine: BaseTypes
%% 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:markdown id: tags:
# Conclusion
* the B language relatively close to the mathematical notation used when teaching theoretical computer science
* the B language supports functional programming, constraint programming, logical inference and proving
* ProB can be used to evaluate, animate, and visualize B (and other formalisms)
* the new Jupyter kernel allows creating interactive, executable documents
* 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`, ...)
notebooks/presentations/img/prob_logo.png

43.5 KiB

0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment