Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
Loading items

Target

Select target project
  • general/stups/prob-teaching-notebooks
1 result
Select Git revision
Loading items
Show changes

Commits on Source 3

%% Cell type:markdown id:7359298e-63ac-4080-9139-aa90c8043b2a tags: %% Cell type:markdown id:7359298e-63ac-4080-9139-aa90c8043b2a tags:
# Introduction to Prolog # Introduction to Prolog
%% Cell type:markdown id:49fd5211 tags: %% Cell type:markdown id:49fd5211 tags:
### Propositions ### Propositions
Prolog programs consist of <b>clauses</b>. Prolog programs consist of <b>clauses</b>.
A clause is always terminated by a dot (```.```). A clause is always terminated by a dot (```.```).
The simplest clauses are facts. Here we define two propositions to be true: The simplest clauses are facts. Here we define two propositions to be true:
%% Cell type:code id:93e05f7b-a91c-4262-861e-a399e094b710 tags: %% Cell type:code id:93e05f7b-a91c-4262-861e-a399e094b710 tags:
``` prolog ``` prolog
rains. rains.
no_hat. no_hat.
``` ```
%% Output
%% Cell type:markdown id:b05ae74b tags: %% Cell type:markdown id:b05ae74b tags:
We can now ask the Prolog system whether it rains: We can now ask the Prolog system whether it rains:
%% Cell type:code id:20b05b2c tags: %% Cell type:code id:20b05b2c tags:
``` prolog ``` prolog
?-rains. ?-rains.
``` ```
%% Output %% Output
%% Cell type:markdown id:50c188fa tags: %% Cell type:markdown id:50c188fa tags:
More complicated clauses make use of the implication operator ```:-```. They are also called rules. Logically they stipulate that the left-hand side of the clause must be true if the right-hand side is true. The right-hand side can contain multiple propositions separated by commas. The comma can be read as a logical conjunction (and). More complicated clauses make use of the implication operator ```:-```. They are also called rules. Logically they stipulate that the left-hand side of the clause must be true if the right-hand side is true. The right-hand side can contain multiple propositions separated by commas. The comma can be read as a logical conjunction (and).
%% Cell type:code id:2b8b84a0 tags: %% Cell type:code id:2b8b84a0 tags:
``` prolog ``` prolog
carry_umbrella :- rains, no_hat. carry_umbrella :- rains, no_hat.
``` ```
%% Output
%% Cell type:code id:4e6314e8 tags: %% Cell type:code id:4e6314e8 tags:
``` prolog ``` prolog
?- carry_umbrella. ?- carry_umbrella.
``` ```
%% Output %% Output
%% Cell type:markdown id:161b0f75 tags: %% Cell type:markdown id:161b0f75 tags:
%% Cell type:markdown id:d7254b1b tags: %% Cell type:markdown id:d7254b1b tags:
### Predicates ### Predicates
Instead of propositions we can also use predicates with arguments within our clauses. The arguments to predicates denote objects for which the predicate is true. Arguments which start with an upper-case letter are logical variables. Below ```X``` is such a variable and it can stand for any object. Instead of propositions we can also use predicates with arguments within our clauses. The arguments to predicates denote objects for which the predicate is true. Arguments which start with an upper-case letter are logical variables. Below ```X``` is such a variable and it can stand for any object.
%% Cell type:code id:1d6eed4f tags: %% Cell type:code id:1d6eed4f tags:
``` prolog ``` prolog
human(sokrates). human(sokrates).
human(schopenhauer). human(schopenhauer).
human(locke). human(locke).
tiger(hobbes). tiger(hobbes).
mortal(X) :- human(X). mortal(X) :- human(X).
mortal(X) :- animal(X). mortal(X) :- animal(X).
animal(X) :- tiger(X). animal(X) :- tiger(X).
``` ```
%% Output
%% Cell type:markdown id:e645f31e tags: %% Cell type:markdown id:e645f31e tags:
You can now ask questions about logical consequences of your logic program. In simple queries you provide all arguments: You can now ask questions about logical consequences of your logic program. In simple queries you provide all arguments:
%% Cell type:code id:a2ab9e95 tags: %% Cell type:code id:a2ab9e95 tags:
``` prolog ``` prolog
?-human(locke). ?-human(locke).
``` ```
%% Output %% Output
%% Cell type:code id:838bc91a tags: %% Cell type:code id:838bc91a tags:
``` prolog ``` prolog
?- human(hobbes). ?- human(hobbes).
``` ```
%% Output %% Output
%% Cell type:code id:4d3217da tags: %% Cell type:code id:4d3217da tags:
``` prolog ``` prolog
?- animal(hobbes). ?- animal(hobbes).
``` ```
%% Output %% Output
%% Cell type:markdown id:c8d0600e tags: %% Cell type:markdown id:c8d0600e tags:
You can also use variables in queries, and Prolog will find values for the variables so that the result is a logical consequence of you program: You can also use variables in queries, and Prolog will find values for the variables so that the result is a logical consequence of you program:
%% Cell type:code id:93e47505 tags: %% Cell type:code id:93e47505 tags:
``` prolog ``` prolog
?- mortal(X). ?- mortal(X).
``` ```
%% Output %% Output
%% Cell type:markdown id:d82e2815 tags: %% Cell type:markdown id:d82e2815 tags:
In the standard Prolog console you can type a semicolong (```;```) to get more answers. Here in Jupyter we need to use ```jupyter:retry```. In the standard Prolog console you can type a semicolong (```;```) to get more answers. Here in Jupyter we need to use ```jupyter:retry```.
%% Cell type:code id:0c4d96e2 tags: %% Cell type:code id:0c4d96e2 tags:
``` prolog ``` prolog
jupyter:retry jupyter:retry
``` ```
%% Output %% Output
%% Cell type:code id:47e57f93 tags: %% Cell type:code id:47e57f93 tags:
``` prolog ``` prolog
jupyter:retry jupyter:retry
``` ```
%% Output %% Output
%% Cell type:code id:7fd70461 tags: %% Cell type:code id:7fd70461 tags:
``` prolog ``` prolog
jupyter:retry jupyter:retry
``` ```
%% Output %% Output
%% Cell type:code id:81724623 tags: %% Cell type:code id:81724623 tags:
``` prolog ``` prolog
jupyter:retry jupyter:retry
``` ```
%% Output %% Output
%% Cell type:markdown id:3dce4ccd tags: %% Cell type:markdown id:3dce4ccd tags:
Jupyter provides a feature to compute all solutions of a goal and display them in a table: Jupyter provides a feature to compute all solutions of a goal and display them in a table:
%% Cell type:code id:4d656338 tags: %% Cell type:code id:4d656338 tags:
``` prolog ``` prolog
jupyter:print_table(mortal(X)) jupyter:print_table(mortal(X))
``` ```
%% Output %% Output
X | X |
:- | :- |
sokrates | sokrates |
schopenhauer | schopenhauer |
locke | locke |
hobbes | hobbes |
%% Cell type:markdown id:d90546b0 tags: %% Cell type:markdown id:d90546b0 tags:
Prolog also has a built-in predicate called ```findall``` which can be used to find all solutions in one go: Prolog also has a built-in predicate called ```findall``` which can be used to find all solutions in one go:
%% Cell type:code id:a7478245 tags: %% Cell type:code id:a7478245 tags:
``` prolog ``` prolog
?-findall(X,mortal(X),Results). ?-findall(X,mortal(X),Results).
``` ```
%% Output %% Output
%% Cell type:markdown id:74c96ce2 tags: %% Cell type:markdown id:74c96ce2 tags:
### Prolog lists and using append ### Prolog lists and using append
The result is a Prolog list. Lists play an important role in Prolog and they can be written using square brackets. ```[]``` denotes the empty list. The built-in predicate ```append``` can be used to concatenate two lists: The result is a Prolog list. Lists play an important role in Prolog and they can be written using square brackets. ```[]``` denotes the empty list. The built-in predicate ```append``` can be used to concatenate two lists:
%% Cell type:code id:0352f53e tags: %% Cell type:code id:0352f53e tags:
``` prolog ``` prolog
?-append([sokrates,locke],[hobbes],R). ?-append([sokrates,locke],[hobbes],R).
``` ```
%% Output %% Output
%% Cell type:markdown id:fd8a78b7 tags: %% Cell type:markdown id:fd8a78b7 tags:
Lists can contain any kind of object, e.g., numbers but also other lists: Lists can contain any kind of object, e.g., numbers but also other lists:
%% Cell type:code id:9e3be61b tags: %% Cell type:code id:9e3be61b tags:
``` prolog ``` prolog
?-append([1,2,sokrates,3],[4,[sokrates],4],Out). ?-append([1,2,sokrates,3],[4,[sokrates],4],Out).
``` ```
%% Output %% Output
%% Cell type:markdown id:db2baf14 tags: %% Cell type:markdown id:db2baf14 tags:
One nice feature of logic programming is that the input/output relation is not pre-determined. One can run predicates backwards, meaning one can use ```append``` to deconstruct a list: One nice feature of logic programming is that the input/output relation is not pre-determined. One can run predicates backwards, meaning one can use ```append``` to deconstruct a list:
%% Cell type:code id:186fe078 tags: %% Cell type:code id:186fe078 tags:
``` prolog ``` prolog
?-append(X,Y,[1,2,3]). ?-append(X,Y,[1,2,3]).
``` ```
%% Output %% Output
%% Cell type:code id:de721f76 tags: %% Cell type:code id:de721f76 tags:
``` prolog ``` prolog
jupyter:retry. jupyter:retry.
``` ```
%% Output %% Output
%% Cell type:code id:ea9e3961 tags: %% Cell type:code id:ea9e3961 tags:
``` prolog ``` prolog
jupyter:retry. jupyter:retry.
``` ```
%% Output %% Output
%% Cell type:code id:e09505d2 tags: %% Cell type:code id:e09505d2 tags:
``` prolog ``` prolog
jupyter:retry. jupyter:retry.
``` ```
%% Output %% Output
%% Cell type:code id:52857ccd tags: %% Cell type:code id:52857ccd tags:
``` prolog ``` prolog
jupyter:retry. jupyter:retry.
``` ```
%% Output %% Output
%% Cell type:markdown id:aacfbf9d tags: %% Cell type:markdown id:aacfbf9d tags:
Variables can also appear multiple times in clauses or queries. Here we check if we can split a list in half: Variables can also appear multiple times in clauses or queries. Here we check if we can split a list in half:
%% Cell type:code id:12f78859 tags: %% Cell type:code id:12f78859 tags:
``` prolog ``` prolog
?-append(X,X,[a,b,a,b]). ?-append(X,X,[a,b,a,b]).
``` ```
%% Output %% Output
%% Cell type:markdown id:16ffb236 tags: %% Cell type:markdown id:16ffb236 tags:
With the underscore we indicate that we are not interested in an argument; it is an anonymous logical variable. Here we use this to find the last element of a list: With the underscore we indicate that we are not interested in an argument; it is an anonymous logical variable. Here we use this to find the last element of a list:
%% Cell type:code id:99bfae95 tags: %% Cell type:code id:99bfae95 tags:
``` prolog ``` prolog
?-append(_,[X],[a,b,c,d]). ?-append(_,[X],[a,b,c,d]).
``` ```
%% Output %% Output
%% Cell type:markdown id:466ece27 tags: %% Cell type:markdown id:466ece27 tags:
### Family tree example ### Family tree example
We now load a Prolog file describing the family tree of "Game of Thrones". We now load a Prolog file describing the family tree of "Game of Thrones".
%% Cell type:code id:5627c07e tags: %% Cell type:code id:5627c07e tags:
``` prolog ``` prolog
:- consult('prolog_files/1_got_family_tree.pl'). :- consult('prolog_files/1_got_family_tree.pl').
``` ```
%% Cell type:markdown id:068e1fdc tags: %% Cell type:markdown id:068e1fdc tags:
It contains facts for four basic predicates male/1, female/1, child/2 and couple/2. It contains facts for four basic predicates male/1, female/1, child/2 and couple/2.
%% Cell type:code id:428e3101 tags: %% Cell type:code id:428e3101 tags:
``` prolog ``` prolog
?-male(X). ?-male(X).
``` ```
%% Output %% Output
%% Cell type:markdown id:c2a8192b tags: %% Cell type:markdown id:c2a8192b tags:
We an now find the parents of X: We an now find the parents of X:
%% Cell type:code id:5134897e tags: %% Cell type:code id:5134897e tags:
``` prolog ``` prolog
?-male(X),child(X,Y). ?-male(X),child(X,Y).
``` ```
%% Output %% Output
%% Cell type:code id:cd9a4bf2 tags: %% Cell type:code id:cd9a4bf2 tags:
``` prolog ``` prolog
jupyter:retry. jupyter:retry.
``` ```
%% Output %% Output
%% Cell type:markdown id:fa7eb5e5 tags: %% Cell type:markdown id:fa7eb5e5 tags:
Let us now define derived predicates for father and mother: Let us now define derived predicates for father and mother:
%% Cell type:code id:edfb9af1 tags: %% Cell type:code id:edfb9af1 tags:
``` prolog ``` prolog
father(A,B) :- child(B,A),male(A). father(A,B) :- child(B,A),male(A).
mother(A,B) :- child(B,A),female(A). mother(A,B) :- child(B,A),female(A).
``` ```
%% Output
%% Cell type:code id:e8aaec06 tags: %% Cell type:code id:e8aaec06 tags:
``` prolog ``` prolog
?-father(A,'Sansa Stark'). ?-father(A,'Sansa Stark').
``` ```
%% Output %% Output
%% Cell type:markdown id:53b594a2 tags: %% Cell type:markdown id:53b594a2 tags:
We can visualise the father/mother relationships in graphical way in Jupyter: We can visualise the father/mother relationships in graphical way in Jupyter:
%% Cell type:code id:d4664fd8 tags: %% Cell type:code id:d4664fd8 tags:
``` prolog ``` prolog
parent_relation(A,B,'father') :- father(A,B). parent_relation(A,B,'father') :- father(A,B).
parent_relation(A,B,'mother') :- mother(A,B). parent_relation(A,B,'mother') :- mother(A,B).
``` ```
%% Output
%% Cell type:code id:08715fa2 tags: %% Cell type:code id:08715fa2 tags:
``` prolog ``` prolog
jupyter:print_transition_graph(parent_relation/3, 1, 2, 3). jupyter:print_transition_graph(parent_relation/3, 1, 2, 3).
``` ```
%% Output %% Output
%% Cell type:markdown id:e2ed5de7 tags: %% Cell type:markdown id:e2ed5de7 tags:
Let us now define the grandfather and grandmother relationships: Let us now define the grandfather and grandmother relationships:
%% Cell type:code id:313194bb tags: %% Cell type:code id:313194bb tags:
``` prolog ``` prolog
grandfather(A,B) :- child(B,C) , child(C,A), male(A). grandfather(A,B) :- child(B,C) , child(C,A), male(A).
grandmother(A,B) :- child(B,C) , child(C,A), female(A). grandmother(A,B) :- child(B,C) , child(C,A), female(A).
``` ```
%% Output
%% Cell type:code id:e0eed7cc tags: %% Cell type:code id:e0eed7cc tags:
``` prolog ``` prolog
?-grandfather(GF,'Sansa Stark'). ?-grandfather(GF,'Sansa Stark').
``` ```
%% Output %% Output
%% Cell type:markdown id:d0e8eb01 tags: %% Cell type:markdown id:d0e8eb01 tags:
Finally let us use recursion in Prolog to define arbitrary ancestors: Finally let us use recursion in Prolog to define arbitrary ancestors:
%% Cell type:code id:c2615402 tags: %% Cell type:code id:c2615402 tags:
``` prolog ``` prolog
parent(A,B) :- child(B,A). parent(A,B) :- child(B,A).
ancestor(A,B):- parent(A,B). ancestor(A,B):- parent(A,B).
ancestor(A,B):- parent(C,B), ancestor(A,C). ancestor(A,B):- parent(C,B), ancestor(A,C).
``` ```
%% Output
%% Cell type:code id:d2b8accc tags: %% Cell type:code id:d2b8accc tags:
``` prolog ``` prolog
?-ancestor(GF,'Sansa Stark'). ?-ancestor(GF,'Sansa Stark').
``` ```
%% Output %% Output
%% Cell type:code id:05f68119 tags: %% Cell type:code id:05f68119 tags:
``` prolog ``` prolog
jupyter:print_table(ancestor(X,'Sansa Stark')) jupyter:print_table(ancestor(X,'Sansa Stark'))
``` ```
%% Output %% Output
X | X |
:- | :- |
Eddard Stark | Eddard Stark |
Catelyn Stark | Catelyn Stark |
Rickard Stark | Rickard Stark |
Lyarra Stark | Lyarra Stark |
%% Cell type:markdown id:e6582326 tags: %% Cell type:markdown id:e6582326 tags:
### Send More Money Puzzle ### Send More Money Puzzle
Prolog is also a natural language to solve constraint satisfaction problems. In particular the CLP(FD) library is very useful here. It allows to solve constraints over finite domains. Prolog is also a natural language to solve constraint satisfaction problems. In particular the CLP(FD) library is very useful here. It allows to solve constraints over finite domains.
%% Cell type:code id:da2e206f tags: %% Cell type:code id:da2e206f tags:
``` prolog ``` prolog
:- use_module(library(clpfd)). :- use_module(library(clpfd)).
``` ```
%% Cell type:markdown id:8d8c47ed tags: %% Cell type:markdown id:8d8c47ed tags:
The library provides a few operators like ```#=```, ```ins``` or ```all_different```: The library provides a few operators like ```#=```, ```ins``` or ```all_different```:
%% Cell type:code id:cf4ff4dd tags: %% Cell type:code id:cf4ff4dd tags:
``` prolog ``` prolog
?- X #= Y+Z, [Y,Z] ins 0..9. ?- X #= Y+Z, [Y,Z] ins 0..9.
``` ```
%% Output %% Output
%% Cell type:markdown id:25e2db2a tags: %% Cell type:markdown id:25e2db2a tags:
To find solutions one needs to call ```labeling```: To find solutions one needs to call ```labeling```:
%% Cell type:code id:4f8aee37 tags: %% Cell type:code id:4f8aee37 tags:
``` prolog ``` prolog
X #= Y+Z, [Y,Z] ins 0..9, labeling([],[Y,Z]). X #= Y+Z, [Y,Z] ins 0..9, labeling([],[Y,Z]).
``` ```
%% Output %% Output
%% Cell type:code id:aac2c0ab tags: %% Cell type:code id:aac2c0ab tags:
``` prolog ``` prolog
X #= Y+Z, [Y,Z] ins 0..9, all_different([X,Y,Z]), labeling([],[Y,Z]). X #= Y+Z, [Y,Z] ins 0..9, all_different([X,Y,Z]), labeling([],[Y,Z]).
``` ```
%% Output %% Output
%% Cell type:markdown id:ae23fbd6 tags: %% Cell type:markdown id:ae23fbd6 tags:
Let us now solve the Send More Money puzzle, where we have to find distinct digits such that this equation holds: Let us now solve the Send More Money puzzle, where we have to find distinct digits such that this equation holds:
``` ```
S E N D S E N D
+ M O R E + M O R E
= M O N E Y = M O N E Y
``` ```
%% Cell type:code id:c86fb33e tags: %% Cell type:code id:c86fb33e tags:
``` prolog ``` prolog
?- L = [S,E,N,D,M,O,R,Y], ?- L = [S,E,N,D,M,O,R,Y],
L ins 0..9, % all variables are digits L ins 0..9, % all variables are digits
S#>0, M#>0, % S and M cannot be 1 S#>0, M#>0, % S and M cannot be 1
all_different(L), % all variables are different all_different(L), % all variables are different
1000*S + 100*E + 10*N + D 1000*S + 100*E + 10*N + D
+ 1000*M + 100*O + 10*R + E + 1000*M + 100*O + 10*R + E
#= 10000*M + 1000*O + 100*N + 10*E + Y, #= 10000*M + 1000*O + 100*N + 10*E + Y,
labeling([], L). labeling([], L).
``` ```
%% Output %% Output
%% Cell type:code id:deaef138 tags: %% Cell type:code id:deaef138 tags:
``` prolog ``` prolog
juptyer:retry juptyer:retry.
``` ```
%% Output %% Output
%% Cell type:markdown id:5f251e4d tags: %% Cell type:markdown id:5f251e4d tags:
%% Cell type:markdown id:701bee1e tags:
%% Cell type:markdown id:c600dcec tags:
%% Cell type:markdown id:058bc4fb tags:
......
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Vorlesung: B Sprache # Vorlesung: B Sprache
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Struktur von Event-B Modellen ## Struktur von Event-B Modellen
Ein Event-B System besteht aus Ein Event-B System besteht aus
* statischen Teilen: die Kontexte * statischen Teilen: die Kontexte
- definieren Konstanten, Basismengen, Axiome, Theoreme - definieren Konstanten, Basismengen, Axiome, Theoreme
* dynamischen Teilen: Maschinen * dynamischen Teilen: Maschinen
- definieren Variablen, Ereignisse, Invarianten - definieren Variablen, Ereignisse, Invarianten
* Kontexte können von Maschinen gesehen werden * Kontexte können von Maschinen gesehen werden
* Kontexte und Maschinen können verfeinert werden * Kontexte und Maschinen können verfeinert werden
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Syntaktische Klassen ## Syntaktische Klassen
Es gibt drei Arten von Formeln in B: Es gibt drei Arten von Formeln in B:
- **Ausdrücke** (Expressions): haben einen Wert, verändern den Zustand einer B Maschine *nicht* - **Ausdrücke** (Expressions): haben einen Wert, verändern den Zustand einer B Maschine *nicht*
- **Prädikate** (Predicates): sind wahr oder falsch, haben *keinen* Wert und verändern den Zustand der Maschine *nicht* - **Prädikate** (Predicates): sind wahr oder falsch, haben *keinen* Wert und verändern den Zustand der Maschine *nicht*
- **Anweisungen** (Substitutions, Statements): haben keinen Wert, können aber den Zustand einer Maschine verändern - **Anweisungen** (Substitutions, Statements): haben keinen Wert, können aber den Zustand einer Maschine verändern
Anweisungen sind zB `x := x+1` und können nur in Maschinen, nicht in Kontexten verwendet werden. Anweisungen sind zB `x := x+1` und können nur in Maschinen, nicht in Kontexten verwendet werden.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Dies ist ein Ausdruck in B: Dies ist ein Ausdruck in B:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2+3 2+3
``` ```
%% Output %% Output
$5$ $5$
5 5
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Dies ist ein Prädikat in B: Dies ist ein Prädikat in B:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>3 2>3
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
B unterscheidet streng zwischen den Bool'schen Werten TRUE und FALSE und zwischen Prädikaten die wahr und falsch sind. Folgendes ist ein valider Ausdruck in B und beschreibt die Menge bestehend aus dem Bool'schen Wert `FALSE`: B unterscheidet streng zwischen den Bool'schen Werten TRUE und FALSE und zwischen Prädikaten die wahr und falsch sind. Folgendes ist ein valider Ausdruck in B und beschreibt die Menge bestehend aus dem Bool'schen Wert `FALSE`:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{FALSE} {FALSE}
``` ```
%% Output %% Output
$\{\mathit{FALSE}\}$ $\{\mathit{FALSE}\}$
{FALSE} {FALSE}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Folgendes ist **kein** valider Ausdruck in B: Folgendes ist **kein** valider Ausdruck in B:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{bool(2>3)} {bool(2>3)}
``` ```
%% Output %% Output
$\{\mathit{FALSE}\}$ $\{\mathit{FALSE}\}$
{FALSE} {FALSE}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Syntax ## Syntax
Die meisten Operatoren in B können entweder als ASCII Zeichenkette oder als Unicode Symbol eingegeben werden. Die meisten Operatoren in B können entweder als ASCII Zeichenkette oder als Unicode Symbol eingegeben werden.
Hier verwenden wir zum Beispiel die Unicode Version von ```/``` für die Division: Hier verwenden wir zum Beispiel die Unicode Version von ```/``` für die Division:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
10 ÷ 2 10 ÷ 2
``` ```
%% Output %% Output
$5$ $5$
5 5
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Syntax von Event-B und klassischem B unterscheidet sich leicht. Die Syntax von Event-B und klassischem B unterscheidet sich leicht.
In Rodin muss man Event-B Syntax verwenden; Jupyter verwendet standardmäßig klassisches B. In Rodin muss man Event-B Syntax verwenden; Jupyter verwendet standardmäßig klassisches B.
Zum Beispiel benutzt Rodin `^` zum Potenzieren, während man im klassische B `**` verwendet: Zum Beispiel benutzt Rodin `^` zum Potenzieren, während man im klassische B `**` verwendet:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2**100 2**100
``` ```
%% Output %% Output
Error from ProB: ERROR Error from ProB: ERROR
2 errors: 2 errors:
Error: Type mismatch: Expected POW(_A), but was INTEGER in '2' Error: Type mismatch: Expected POW(_A), but was INTEGER in '2'
Error: Type mismatch: Expected POW(_A), but was INTEGER in '100' Error: Type mismatch: Expected POW(_A), but was INTEGER in '100'
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In Rodin wird `**` für das kartesische Produkt verwendet, im klassischen B verwendet man dafür `*`. In Rodin wird `**` für das kartesische Produkt verwendet, im klassischen B verwendet man dafür `*`.
Wir laden jetzt ein leeres Event-B Modell um den Parser in den Event-B Modus zu wechseln. Wir laden jetzt ein leeres Event-B Modell um den Parser in den Event-B Modus zu wechseln.
Man kann auch das Kommando ```:language event_b``` verwenden um den Parser umzustellen. Man kann auch das Kommando ```:language event_b``` verwenden um den Parser umzustellen.
Mit ```:language classical_b``` kann man zurück zum normalen B Parser wechseln. Mit ```:language classical_b``` kann man zurück zum normalen B Parser wechseln.
Wenn man eine B Maschine oder einen Kontext lädt wechselt der Parser in den richtigen Modus. Wenn man eine B Maschine oder einen Kontext lädt wechselt der Parser in den richtigen Modus.
Hier laden wir einen leeren Event-B Kontext; dadurch wechselt der Parser in den Event-B Modus: Hier laden wir einen leeren Event-B Kontext; dadurch wechselt der Parser in den Event-B Modus:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:load models/empty_ctx.eventb :load models/empty_ctx.eventb
``` ```
%% Output %% Output
Loaded machine: empty_ctx Loaded machine: empty_ctx
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2^100 2^100
``` ```
%% Output %% Output
$1267650600228229401496703205376$ $1267650600228229401496703205376$
1267650600228229401496703205376 1267650600228229401496703205376
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Semantische Grundlage von B ## Semantische Grundlage von B
* Arithmetik (ganze Zahlen) ÷ + − ≤ * Arithmetik (ganze Zahlen) ÷ + − ≤
* Prädikatenlogik ⇒ ∀ * Prädikatenlogik ⇒ ∀
* Mengentheorie ∩ ∪ ⊆ ∈ * Mengentheorie ∩ ∪ ⊆ ∈
* Paare * Paare
* Relationen,Funktionen, Sequenzen/Folgen, Bäume * Relationen,Funktionen, Sequenzen/Folgen, Bäume
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Aussagenlogik ## Aussagenlogik
B unterstützt folgende Junktoren der Aussagenlogik: B unterstützt folgende Junktoren der Aussagenlogik:
Junktor | ASCII | Unicode Junktor | ASCII | Unicode
-------|-------|----- -------|-------|-----
Konjunktion | & | ∧ Konjunktion | & | ∧
Disjunktion | or | ∨ Disjunktion | or | ∨
Negation | not | ¬ Negation | not | ¬
Implikation | => | ⇒ Implikation | => | ⇒
Äquivalenz | <=> | ⇔ Äquivalenz | <=> | ⇔
Mit `:prettyprint` kann man sich die Unicode Version einer Formel ausgeben lassen: Mit `:prettyprint` kann man sich die Unicode Version einer Formel ausgeben lassen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:prettyprint not(2>3 or 4>2) <=> 5>2 :prettyprint not(2>3 or 4>2) <=> 5>2
``` ```
%% Output %% Output
$\neg (2 > 3 \vee 4 > 2) \mathbin\Leftrightarrow 5 > 2$ $\neg (2 > 3 \vee 4 > 2) \mathbin\Leftrightarrow 5 > 2$
¬(2 > 3 ∨ 4 > 2) ⇔ 5 > 2 ¬(2 > 3 ∨ 4 > 2) ⇔ 5 > 2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann eine Aussage natürlich auch auswerten: Man kann eine Aussage natürlich auch auswerten:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
not(2>3 or 4>2) ⇔ 5>2 not(2>3 or 4>2) ⇔ 5>2
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>3 or 4>2 2>3 or 4>2
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
not(2>3 or 4>2) not(2>3 or 4>2)
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
5>2 5>2
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Prioritäten ### Prioritäten
* höchste Priorität: ¬ * höchste Priorität: ¬
* danach ∧ , ∨ * danach ∧ , ∨
* danach ⇒ , ⇔ * danach ⇒ , ⇔
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>0 or 3>4 ⇒ 4>5 2>0 or 3>4 ⇒ 4>5
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>0 or (3>4 ⇒ 4>5) 2>0 or (3>4 ⇒ 4>5)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(2>0 or 3>4) ⇒ 4>5 (2>0 or 3>4) ⇒ 4>5
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1=1 => 2=2) => 3=1 (1=1 => 2=2) => 3=1
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
*Achtung:* *Achtung:*
* in Rodin/Event-B haben Konjunktion und Disjunktion die gleiche Priorität und dürfen nicht ohne Klammerung gemischt werden. In klassischem B schon. * in Rodin/Event-B haben Konjunktion und Disjunktion die gleiche Priorität und dürfen nicht ohne Klammerung gemischt werden. In klassischem B schon.
* Das gleiche gilt für => und <=>. * Das gleiche gilt für => und <=>.
* In Rodin ist auch keine Assoziativität für => oder <=> definiert worden. Man darf diese Operatoren also auch nicht untereinander ohne Klammern mischen. * In Rodin ist auch keine Assoziativität für => oder <=> definiert worden. Man darf diese Operatoren also auch nicht untereinander ohne Klammern mischen.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2>1 or 2>3 & 3>4 2>1 or 2>3 & 3>4
``` ```
%% Output %% Output
de.prob.animator.domainobjects.EvaluationException: Could not parse formula: de.prob.animator.domainobjects.EvaluationException: Could not parse formula:
Parsing predicate failed because: Operator: ∨ is not compatible with: ∧, parentheses are required Parsing predicate failed because: Operator: ∨ is not compatible with: ∧, parentheses are required
Operator: ∨ is not compatible with: ∧, parentheses are required Operator: ∨ is not compatible with: ∧, parentheses are required
Parsing expression failed because: Operator: ∨ is not compatible with: ∧, parentheses are required Parsing expression failed because: Operator: ∨ is not compatible with: ∧, parentheses are required
Operator: ∨ is not compatible with: ∧, parentheses are required Operator: ∨ is not compatible with: ∧, parentheses are required
Parsing substitution failed because: Unknown operator: (expected to find an assignment operator) Parsing substitution failed because: Unknown operator: (expected to find an assignment operator)
Unknown operator: (expected to find an assignment operator) Unknown operator: (expected to find an assignment operator)
Code: 2>1 or 2>3 & 3>4 Code: 2>1 or 2>3 & 3>4
Unicode translation: 2>1 ∨ 2>3 ∧ 3>4 Unicode translation: 2>1 ∨ 2>3 ∧ 3>4
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Prädikate ## Prädikate
In Event-B gibt es die Aussagen true (⊤) und false (⊥) (nicht verwechseln mit den Bool'schen Datenwerten TRUE und FALSE). Im klassichen B gibt es diese beiden Aussagen nicht (wobei ProB `btrue` und `bfalse` akzeptiert). In Event-B gibt es die Aussagen true (⊤) und false (⊥) (nicht verwechseln mit den Bool'schen Datenwerten TRUE und FALSE). Im klassichen B gibt es diese beiden Aussagen nicht (wobei ProB `btrue` und `bfalse` akzeptiert).
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
true or false true or false
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
⊤ or ⊥ ⊤ or ⊥
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wahrheitswerte können über Prädikate hergestellt werden: Wahrheitswerte können über Prädikate hergestellt werden:
* ein n-äres Pradikat bekommt n Datenwerte und bildet diese auf einen Wahrheitswert ab * ein n-äres Pradikat bekommt n Datenwerte und bildet diese auf einen Wahrheitswert ab
Für alle Datentypen gibt es die binären Pradikate = und ≠ (wobei gilt x ≠ y ⇔ ¬(x=y)). Für alle Datentypen gibt es die binären Pradikate = und ≠ (wobei gilt x ≠ y ⇔ ¬(x=y)).
Für Zahlen gibt es die mathematischen Vergleichsoperatoren. Für Mengen werden noch weitere Prädikate hinzukommen. Für Zahlen gibt es die mathematischen Vergleichsoperatoren. Für Mengen werden noch weitere Prädikate hinzukommen.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
2 = 3-1 2 = 3-1
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
3 ≠ 3+1 3 ≠ 3+1
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
4 >= 2+2 4 >= 2+2
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Quantoren ## Quantoren
In B gibt es zwei Quantoren die neue Variablen einführen: In B gibt es zwei Quantoren die neue Variablen einführen:
* den Existenzquantor (mindestens eins) * den Existenzquantor (mindestens eins)
- #x.(P) als ASCII - #x.(P) als ASCII
- ∃x.(P) als Unicode - ∃x.(P) als Unicode
* den Allquantor/Universalquantor (alle / jeder) * den Allquantor/Universalquantor (alle / jeder)
- !x.(P => Q) als ASCII - !x.(P => Q) als ASCII
- ∀(x).(P ⇒ Q) als Unicode - ∀(x).(P ⇒ Q) als Unicode
Der Rumpf eines Allquantors muss also immer eine Implikation auf oberster Ebene verwenden. Der Rumpf eines Allquantors muss also immer eine Implikation auf oberster Ebene verwenden.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∃x .( x>2 ) ∃x .( x>2 )
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∀x .( x>2 ⇒ x>3 ) ∀x .( x>2 ⇒ x>3 )
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
**Solution:** **Solution:**
* $\mathit{x} = 3$ * $\mathit{x} = 3$
FALSE FALSE
Solution: Solution:
x = 3 x = 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∀x .( x>2 & x < 100 ⇒ ∃y.(x=y+y)) ∀x .( x>2 & x < 100 ⇒ ∃y.(x=y+y))
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
**Solution:** **Solution:**
* $\mathit{x} = 3$ * $\mathit{x} = 3$
FALSE FALSE
Solution: Solution:
x = 3 x = 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∀x .( x>2 & x < 100 ⇒ ∃y.(x=y+y) or ∃y.(x=y+y+1)) ∀x .( x>2 & x < 100 ⇒ ∃y.(x=y+y) or ∃y.(x=y+y+1))
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Typisierung bei Quantoren ### Typisierung bei Quantoren
B basiert auf typisierter Logik B basiert auf typisierter Logik
* Bei Quantoren, zum Beispiel, müssen die neuen Variablen typisiert werden * Bei Quantoren, zum Beispiel, müssen die neuen Variablen typisiert werden
- ∃x.(2>3) ist nicht erlaubt - ∃x.(2>3) ist nicht erlaubt
Generell: für ∃x.(P) und ∀(x).(P ⇒ Q) muss P den Typen von x bestimmbar machen. Generell: für ∃x.(P) und ∀(x).(P ⇒ Q) muss P den Typen von x bestimmbar machen.
Deshalb ist der Rumpf eines Allquantors auch immer eine Implikation. Deshalb ist der Rumpf eines Allquantors auch immer eine Implikation.
Beim Existenzquantor wird oft eine Konjunktion verwendet. Beim Existenzquantor wird oft eine Konjunktion verwendet.
Warum macht eine Implikation beim Existenzquantor fast nie Sinn? Warum macht eine Implikation beim Existenzquantor fast nie Sinn?
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∃x.(x>-100000 => 22=1) ∃x.(x>-100000 => 22=1)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Arithmetik ## Arithmetik
B bietet Arithmetik über *ganzen* Zahlen an. B bietet Arithmetik über *ganzen* Zahlen an.
Folgende Zahlenmengen sind vordefiniert: Folgende Zahlenmengen sind vordefiniert:
* INT, ℤ * INT, ℤ
* NAT = {x|x≥0}, ℕ * NAT = {x|x≥0}, ℕ
* NAT1= {x|x≥1}, ℕ1 * NAT1= {x|x≥1}, ℕ1
In Atelier-B (klassisches B für die Softwareentwicklung, nicht in Rodin) wird zwischen mathematischen und implementierbaren Zahlen unterschieden: In Atelier-B (klassisches B für die Softwareentwicklung, nicht in Rodin) wird zwischen mathematischen und implementierbaren Zahlen unterschieden:
* Mathematische ganze Zahlen: INTEGER, NATURAL, NATURAL1 * Mathematische ganze Zahlen: INTEGER, NATURAL, NATURAL1
* Implementierbare ganze Zahlen: INT, NAT, NAT1 * Implementierbare ganze Zahlen: INT, NAT, NAT1
* MININT, MAXINT * MININT, MAXINT
NATURAL aus dem klassischem B entspricht also NAT in Rodin. NATURAL aus dem klassischem B entspricht also NAT in Rodin.
NAT aus dem klassischen B entspricht 0..MAXINT in Rodin, wobei MAXINT als Konstante definiert werden muss. NAT aus dem klassischen B entspricht 0..MAXINT in Rodin, wobei MAXINT als Konstante definiert werden muss.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
0:ℕ 0:ℕ
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
0:NAT1 0:NAT1
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Divsion ### Divsion
B benutzt ganzzahlige Division und es gilt zB das Gesetz B benutzt ganzzahlige Division und es gilt zB das Gesetz
* b≠0 ⇒ a ÷ b = (−a) ÷ (−b) * b≠0 ⇒ a ÷ b = (−a) ÷ (−b)
Man hat auch: Man hat auch:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
3/2 3/2
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
-3 / 2 -3 / 2
``` ```
%% Output %% Output
$-1$ $-1$
−1 −1
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In Python bekommt man In Python bekommt man
``` ```
>>> (-3)//2 >>> (-3)//2
-2 -2
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Division durch 0 und modulo durch negative Zahlen ist nicht definiert. Division durch 0 und modulo durch negative Zahlen ist nicht definiert.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
100 mod -2 100 mod -2
``` ```
%% Output %% Output
:eval: NOT-WELL-DEFINED: :eval: NOT-WELL-DEFINED:
mod not defined for negative numbers: 100 mod-2 mod not defined for negative numbers: 100 mod-2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Mengen ## Mengen
Mengen sind ein fundamentales Konzept in B. Mengen sind ein fundamentales Konzept in B.
In eine Mengen darf man nur Werten eines gleichen Typs packen. In eine Mengen darf man nur Werten eines gleichen Typs packen.
Mengen dürfen aber verschachtelt werden. Mengen dürfen aber verschachtelt werden.
Die einfachste Menge ist die leere Menge: Die einfachste Menge ist die leere Menge:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{} {}
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$ $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann Mengen durch **explizite Aufzählung** (Enumeration, set extension auf Englisch) definieren: Man kann Mengen durch **explizite Aufzählung** (Enumeration, set extension auf Englisch) definieren:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1,1+1,2,2+2,3,4} {1,1+1,2,2+2,3,4}
``` ```
%% Output %% Output
$\{1,2,3,4\}$ $\{1,2,3,4\}$
{1,2,3,4} {1,2,3,4}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Mengen können auch mit Hilfe eines Prädikats definiert werden (set comprehension auf Englisch). Die Syntaxform ist `{x | P}`. Mengen können auch mit Hilfe eines Prädikats definiert werden (set comprehension auf Englisch). Die Syntaxform ist `{x | P}`.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x | x>0 & x<5} {x | x>0 & x<5}
``` ```
%% Output %% Output
$\{1,2,3,4\}$ $\{1,2,3,4\}$
{1,2,3,4} {1,2,3,4}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x|x>2+2} {x|x>2+2}
``` ```
%% Output %% Output
$\{\mathit{x}\mid\mathit{x} > 4\}$ $\{\mathit{x}\mid\mathit{x} > 4\}$
{x∣x > 4} {x∣x > 4}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Eine Menge an Zahlen kann auch mit der Intervallnotation ``a..b`` definiert werden: Eine Menge an Zahlen kann auch mit der Intervallnotation ``a..b`` definiert werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..4 1..4
``` ```
%% Output %% Output
$\{1,2,3,4\}$ $\{1,2,3,4\}$
{1,2,3,4} {1,2,3,4}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Kardinalität (Mächtigkeit) einer endlichen Menge kann mit dem card Operator bestimmt werden: Die Kardinalität (Mächtigkeit) einer endlichen Menge kann mit dem card Operator bestimmt werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({1,1+1,2,2+2,3,4}) card({1,1+1,2,2+2,3,4})
``` ```
%% Output %% Output
$4$ $4$
4 4
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({x|x>2}) card({x|x>2})
``` ```
%% Output %% Output
:eval: NOT-WELL-DEFINED: Error from ProB: NOT-WELL-DEFINED
card applied to very large set, cardinality not representable in ProB: closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(none)])) Error: card applied to infinite set, cardinality not representable in ProB: {x|x > 2} (:1:0 to 1:13)
card({x|x>2})
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Mengen können andere Mengen beinhalten: Mengen können andere Mengen beinhalten:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{ 1..4 , {1,2,3,4,2+2}, {}} { 1..4 , {1,2,3,4,2+2}, {}}
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1,2,3,4\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1,2,3,4\}\}$
{∅,{1,2,3,4}} {∅,{1,2,3,4}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({ 1..4 , {1,2,3,4,2+2}, {}}) card({ 1..4 , {1,2,3,4,2+2}, {}})
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Was ist der Untschied zwischen der leeren Menge ∅ und { ∅ }? Was ist der Untschied zwischen der leeren Menge ∅ und { ∅ }?
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∅ = {∅} ∅ = {∅}
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(∅) card(∅)
``` ```
%% Output %% Output
$0$ $0$
0 0
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({∅}) card({∅})
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
∅ : {∅} ∅ : {∅}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Notation `{x | P}` wobei eine Menge per Prädikat definiert wird ist die mächtigste Notation. Die Notation `{x | P}` wobei eine Menge per Prädikat definiert wird ist die mächtigste Notation.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x | x>1 & x<1 } {x | x>1 & x<1 }
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$ $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x | x=1 or x=2 } {x | x=1 or x=2 }
``` ```
%% Output %% Output
$\{1,2\}$ $\{1,2\}$
{1,2} {1,2}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x | x>=1 & x<=4 } {x | x>=1 & x<=4 }
``` ```
%% Output %% Output
$\{1,2,3,4\}$ $\{1,2,3,4\}$
{1,2,3,4} {1,2,3,4}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
NAT = {x | x>=0 } NAT = {x | x>=0 }
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In Event-B gibt es auch eine angepasste Variante der Notation `{x . P | E}`, wo man einen Ausdruck `E` angibt der in die generierte Menge eingefügt wird: In Event-B gibt es auch eine angepasste Variante der Notation `{x . P | E}`, wo man einen Ausdruck `E` angibt der in die generierte Menge eingefügt wird:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x.x:1..10|x*x} {x.x:1..10|x*x}
``` ```
%% Output %% Output
$\{1,4,9,16,25,36,49,64,81,100\}$ $\{1,4,9,16,25,36,49,64,81,100\}$
{1,4,9,16,25,36,49,64,81,100} {1,4,9,16,25,36,49,64,81,100}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Prädikate über Mengen ## Prädikate über Mengen
Es gibt die Standardprädikate der Mathematik: Es gibt die Standardprädikate der Mathematik:
* *
* *
* *
* *
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:prettyprint not({1,2,3} /<<: {1,2,3}) :prettyprint not({1,2,3} /<<: {1,2,3})
``` ```
%% Output %% Output
$\neg (\{1,2,3\} \not\subset \{1,2,3\})$ $\neg (\{1,2,3\} \not\subset \{1,2,3\})$
¬({1,2,3} ⊄ {1,2,3}) ¬({1,2,3} ⊄ {1,2,3})
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Zusätzlich hat Event-B das partition Prädikat, welches wir weiter unter erklären. Zusätzlich hat Event-B das partition Prädikat, welches wir weiter unter erklären.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Operatoren über Mengen ## Operatoren über Mengen
* Vereinigung \/ * Vereinigung \/
* Schnittmenge /\ * Schnittmenge /\
* Differenzmenge \ * Differenzmenge \
* union(S), inter(S) für Menge von Mengen * union(S), inter(S) für Menge von Mengen
* POW(S) (Potenzmenge: Untermengen von S) * POW(S) (Potenzmenge: Untermengen von S)
* POW1(S) (nicht leeren Untermengen von S) * POW1(S) (nicht leeren Untermengen von S)
Übung: diese Operatoren durch comprehension sets definieren Übung: diese Operatoren durch comprehension sets definieren
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
a = {1,2,4} & b = {2,3,4} & aub1 = a \/ b & a = {1,2,4} & b = {2,3,4} & aub1 = a \/ b &
aub2 = {x | x:a or x:b} aub2 = {x | x:a or x:b}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{a} = \{1,2,4\}$ * $\mathit{a} = \{1,2,4\}$
* $\mathit{b} = \{2,3,4\}$ * $\mathit{b} = \{2,3,4\}$
* $\mathit{aub2} = \{1,2,3,4\}$ * $\mathit{aub2} = \{1,2,3,4\}$
* $\mathit{aub1} = \{1,2,3,4\}$ * $\mathit{aub1} = \{1,2,3,4\}$
TRUE TRUE
Solution: Solution:
a = {1,2,4} a = {1,2,4}
b = {2,3,4} b = {2,3,4}
aub2 = {1,2,3,4} aub2 = {1,2,3,4}
aub1 = {1,2,3,4} aub1 = {1,2,3,4}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
a = {1,2,4} & b = {2,3,4} & aib1 = a/\b & a = {1,2,4} & b = {2,3,4} & aib1 = a/\b &
aib2 = {x | x:a & x:b} aib2 = {x | x:a & x:b}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{a} = \{1,2,4\}$ * $\mathit{a} = \{1,2,4\}$
* $\mathit{b} = \{2,3,4\}$ * $\mathit{b} = \{2,3,4\}$
* $\mathit{aib2} = \{2,4\}$ * $\mathit{aib2} = \{2,4\}$
* $\mathit{aib1} = \{2,4\}$ * $\mathit{aib1} = \{2,4\}$
TRUE TRUE
Solution: Solution:
a = {1,2,4} a = {1,2,4}
b = {2,3,4} b = {2,3,4}
aib2 = {2,4} aib2 = {2,4}
aib1 = {2,4} aib1 = {2,4}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
a = {1,2,4} & b = {2,3,4} & aib1 = a \ b a = {1,2,4} & b = {2,3,4} & aib1 = a \ b
& aib2 = {x | x:a & x/:b} & aib2 = {x | x:a & x/:b}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{a} = \{1,2,4\}$ * $\mathit{a} = \{1,2,4\}$
* $\mathit{b} = \{2,3,4\}$ * $\mathit{b} = \{2,3,4\}$
* $\mathit{aib2} = \{1\}$ * $\mathit{aib2} = \{1\}$
* $\mathit{aib1} = \{1\}$ * $\mathit{aib1} = \{1\}$
TRUE TRUE
Solution: Solution:
a = {1,2,4} a = {1,2,4}
b = {2,3,4} b = {2,3,4}
aib2 = {1} aib2 = {1}
aib1 = {1} aib1 = {1}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x.x:1..10|x*x} {x.x:1..10|x*x}
``` ```
%% Output %% Output
$\{1,4,9,16,25,36,49,64,81,100\}$ $\{1,4,9,16,25,36,49,64,81,100\}$
{1,4,9,16,25,36,49,64,81,100} {1,4,9,16,25,36,49,64,81,100}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
a = {1,2,4} & b = {2,3,4} & c = {4,6} & abc = union({a,b,c}) a = {1,2,4} & b = {2,3,4} & c = {4,6} & abc = union({a,b,c})
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{a} = \{1,2,4\}$ * $\mathit{a} = \{1,2,4\}$
* $\mathit{b} = \{2,3,4\}$ * $\mathit{b} = \{2,3,4\}$
* $\mathit{c} = \{4,6\}$ * $\mathit{c} = \{4,6\}$
* $\mathit{abc} = \{1,2,3,4,6\}$ * $\mathit{abc} = \{1,2,3,4,6\}$
TRUE TRUE
Solution: Solution:
a = {1,2,4} a = {1,2,4}
b = {2,3,4} b = {2,3,4}
c = {4,6} c = {4,6}
abc = {1,2,3,4,6} abc = {1,2,3,4,6}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
POW(1..2) POW(1..2)
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$
{∅,{1},{1,2},{2}} {∅,{1},{1,2},{2}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
POW(BOOL) POW(BOOL)
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\}$
{∅,{FALSE},{FALSE,TRUE},{TRUE}} {∅,{FALSE},{FALSE,TRUE},{TRUE}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
POW(POW(BOOL)) POW(POW(BOOL))
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\emptyset\},\{\emptyset,\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{TRUE}\}\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\emptyset\},\{\emptyset,\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{TRUE}\}\}\}$
{∅,{∅},{∅,{FALSE}},{∅,{FALSE,TRUE}},{∅,{TRUE}},{{FALSE}},{∅,{FALSE},{FALSE,TRUE}},{∅,{FALSE},{TRUE}},{{FALSE},{FALSE,TRUE}},{{FALSE},{TRUE}},{∅,{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE}},{∅,{FALSE,TRUE},{TRUE}},{{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE},{TRUE}},{{TRUE}}} {∅,{∅},{∅,{FALSE}},{∅,{FALSE,TRUE}},{∅,{TRUE}},{{FALSE}},{∅,{FALSE},{FALSE,TRUE}},{∅,{FALSE},{TRUE}},{{FALSE},{FALSE,TRUE}},{{FALSE},{TRUE}},{∅,{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE}},{∅,{FALSE,TRUE},{TRUE}},{{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE},{TRUE}},{{TRUE}}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(POW(POW(POW(BOOL)))) card(POW(POW(POW(BOOL))))
``` ```
%% Output %% Output
$65536$ $65536$
65536 65536
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Übung: Send More Money ## Übung: Send More Money
Man soll 8 Ziffern finden so dass folgende Summe aufgeht Man soll 8 Ziffern finden so dass folgende Summe aufgeht
| | | | | | | | | | | | | |
|---|---|---|---|---|---| |---|---|---|---|---|---|
| | | S | E | N | D | | | | S | E | N | D |
| | + | M | O | R | E | | | + | M | O | R | E |
| = | M | O | N | E | Y | | = | M | O | N | E | Y |
Wir brauchen acht Ziffern: Wir brauchen acht Ziffern:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y}<:0..9 {S,E,N,D,M,O,R,Y}<:0..9
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 0$ * $\mathit{R} = 0$
* $\mathit{S} = 0$ * $\mathit{S} = 0$
* $\mathit{D} = 0$ * $\mathit{D} = 0$
* $\mathit{E} = 0$ * $\mathit{E} = 0$
* $\mathit{Y} = 0$ * $\mathit{Y} = 0$
* $\mathit{M} = 0$ * $\mathit{M} = 0$
* $\mathit{N} = 0$ * $\mathit{N} = 0$
* $\mathit{O} = 0$ * $\mathit{O} = 0$
TRUE TRUE
Solution: Solution:
R = 0 R = 0
S = 0 S = 0
D = 0 D = 0
E = 0 E = 0
Y = 0 Y = 0
M = 0 M = 0
N = 0 N = 0
O = 0 O = 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Diese Ziffern sollen alle unterschiedlich sein: Diese Ziffern sollen alle unterschiedlich sein:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 2$ * $\mathit{R} = 2$
* $\mathit{S} = 0$ * $\mathit{S} = 0$
* $\mathit{D} = 5$ * $\mathit{D} = 5$
* $\mathit{E} = 7$ * $\mathit{E} = 7$
* $\mathit{Y} = 1$ * $\mathit{Y} = 1$
* $\mathit{M} = 4$ * $\mathit{M} = 4$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 3$ * $\mathit{O} = 3$
TRUE TRUE
Solution: Solution:
R = 2 R = 2
S = 0 S = 0
D = 5 D = 5
E = 7 E = 7
Y = 1 Y = 1
M = 4 M = 4
N = 6 N = 6
O = 3 O = 3
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Ziffern S und M dürfen nicht 0 sein: Die Ziffern S und M dürfen nicht 0 sein:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 & {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
S /= 0 & M /= 0 S /= 0 & M /= 0
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 3$ * $\mathit{R} = 3$
* $\mathit{S} = 2$ * $\mathit{S} = 2$
* $\mathit{D} = 5$ * $\mathit{D} = 5$
* $\mathit{E} = 7$ * $\mathit{E} = 7$
* $\mathit{Y} = 0$ * $\mathit{Y} = 0$
* $\mathit{M} = 1$ * $\mathit{M} = 1$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 4$ * $\mathit{O} = 4$
TRUE TRUE
Solution: Solution:
R = 3 R = 3
S = 2 S = 2
D = 5 D = 5
E = 7 E = 7
Y = 0 Y = 0
M = 1 M = 1
N = 6 N = 6
O = 4 O = 4
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Und jetzt muss noch die Summe stimmen: Und jetzt muss noch die Summe stimmen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D,M,O,R,Y}<:0..9 & card({S,E,N,D,M,O,R,Y}) = 8 & {S,E,N,D,M,O,R,Y}<:0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
S /= 0 & M /= 0 & S /= 0 & M /= 0 &
S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y M*10000 + O*1000 + N*100 + E*10 + Y
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 8$ * $\mathit{R} = 8$
* $\mathit{S} = 9$ * $\mathit{S} = 9$
* $\mathit{D} = 7$ * $\mathit{D} = 7$
* $\mathit{E} = 5$ * $\mathit{E} = 5$
* $\mathit{Y} = 2$ * $\mathit{Y} = 2$
* $\mathit{M} = 1$ * $\mathit{M} = 1$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 0$ * $\mathit{O} = 0$
TRUE TRUE
Solution: Solution:
R = 8 R = 8
S = 9 S = 9
D = 7 D = 7
E = 5 E = 5
Y = 2 Y = 2
M = 1 M = 1
N = 6 N = 6
O = 0 O = 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir können auch die Menge aller Lösungen bestimmen: Wir können auch die Menge aller Lösungen bestimmen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {S|->E|->N|->D|->M|->O|->R|->Y | :table {S|->E|->N|->D|->M|->O|->R|->Y |
{S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 & {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
S /= 0 & M /= 0 & S /= 0 & M /= 0 &
S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E
= M*10000 + O*1000 + N*100 + E*10 + Y } = M*10000 + O*1000 + N*100 + E*10 + Y }
``` ```
%% Output %% Output
|S|E|N|D|M|O|R|Y| |S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---| |---|---|---|---|---|---|---|---|
|9|5|6|7|1|0|8|2| |9|5|6|7|1|0|8|2|
S E N D M O R Y S E N D M O R Y
9 5 6 7 1 0 8 2 9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Das Partition Prädikat ## Das Partition Prädikat
Dieses Prädikat gibt es nur in Event-B und es ist syntaktischer Zucker für einen grösseren äquivalenten Ausdruck: Dieses Prädikat gibt es nur in Event-B und es ist syntaktischer Zucker für einen grösseren äquivalenten Ausdruck:
``` ```
partition(S,S1,S2,...,Sn) partition(S,S1,S2,...,Sn)
``` ```
steht für steht für
``` ```
S = S1 \/ S2 \/ ... Sn & S = S1 \/ S2 \/ ... Sn &
S1 /\ S2 = {} & ... S1 /\ Sn = {} & S1 /\ S2 = {} & ... S1 /\ Sn = {} &
S2 /\ S3 = {} & ... S2 /\ Sn = {} S2 /\ S3 = {} & ... S2 /\ Sn = {}
... ...
Sn-1 /\ Sn = {} Sn-1 /\ Sn = {}
``` ```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:language event_b :language event_b
``` ```
%% Output %% Output
Changed language for user input to Event-B (forced) Changed language for user input to Event-B (forced)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
partition(1..3,{1},{2},{3}) partition(1..3,{1},{2},{3})
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {a|->b| partition(1..2,a,b)} :table {a|->b| partition(1..2,a,b)}
``` ```
%% Output %% Output
|a|b| |a|b|
|---|---| |---|---|
|∅|{1,2}| |∅|{1,2}|
|{1}|{2}| |{1}|{2}|
|{1,2}|∅| |{1,2}|∅|
|{2}|{1}| |{2}|{1}|
a b a b
{} {1,2} {} {1,2}
{1} {2} {1} {2}
{1,2} {} {1,2} {}
{2} {1} {2} {1}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Neue Basismengen ## Neue Basismengen
Vom Benutzer können in Event-B neue Basismengen eingeführt werden Vom Benutzer können in Event-B neue Basismengen eingeführt werden
* werden in der `sets` Sektion von Kontexten eingeführt * werden in der `sets` Sektion von Kontexten eingeführt
* jede Benutzermenge ist sein eigener Typ! * jede Benutzermenge ist sein eigener Typ!
Man darf unterschiedliche Mengen bzw. Elemente aus unterschiedlichen Basismengen nicht mischen. Man darf unterschiedliche Mengen bzw. Elemente aus unterschiedlichen Basismengen nicht mischen.
Es gibt zwei Möglichkeiten: Es gibt zwei Möglichkeiten:
1) Enumerated Set: man gibt explizit alle Elemente der neuen Basismenge an 1) Enumerated Set: man gibt explizit alle Elemente der neuen Basismenge an
S = {a,b,c} in klassischem B oder partition(S,{a},{b},{c}). S = {a,b,c} in klassischem B oder partition(S,{a},{b},{c}).
2) Deferred Set: man lässt die Menge für Erweiterungen offen 2) Deferred Set: man lässt die Menge für Erweiterungen offen
In Rodin gibt es zwei Wizards zum einführen von enumerated bzw. deferred "carrier" sets. In Rodin gibt es zwei Wizards zum einführen von enumerated bzw. deferred "carrier" sets.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Typen in B ## Typen in B
* es gibt einen Typ für alle Zahlen: INT (ℤ) * es gibt einen Typ für alle Zahlen: INT (ℤ)
* es gibt den Typ BOOL für die Bool'schen Werte * es gibt den Typ BOOL für die Bool'schen Werte
* für jede Basismenge gibt es einen eigenen Typen * für jede Basismenge gibt es einen eigenen Typen
* ist t ein Typ, dann ist POW(t) auch ein Typ * ist t ein Typ, dann ist POW(t) auch ein Typ
* nächste Woche werden wir noch ein weitere Typkonstruktion sehen * nächste Woche werden wir noch ein weitere Typkonstruktion sehen
Jeder Ausdruck und damit auch jede Variable muss genau einen Typen haben. Die Typen müssen mit den Signaturen der B Operatoren kompatibel sein. Jeder Ausdruck und damit auch jede Variable muss genau einen Typen haben. Die Typen müssen mit den Signaturen der B Operatoren kompatibel sein.
* man kann explizit Typen angeben, mit einem Prädikat `VARIABLE ∈ TYP`, zum Beispiel: `a∈ℤ` * man kann explizit Typen angeben, mit einem Prädikat `VARIABLE ∈ TYP`, zum Beispiel: `a∈ℤ`
* oder auf die Typ-Inferenz von Atelier-B, Rodin, ProB hoffen (Atelier-B am schwächsten; ProB am mächtigsten) * oder auf die Typ-Inferenz von Atelier-B, Rodin, ProB hoffen (Atelier-B am schwächsten; ProB am mächtigsten)
Beispiele: Beispiele:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:type 1 :type 1
``` ```
%% Output %% Output
INT INT
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1 ∈ ℤ 1 ∈ ℤ
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:type {1} :type {1}
``` ```
%% Output %% Output
POW(INT) POW(INT)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1} ∈ POW(INT) {1} ∈ POW(INT)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
NAT : POW(INT) NAT : POW(INT)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:type {} :type {}
``` ```
%% Output %% Output
POW(?) POW(?)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Are the following two expressions well-typed? What are the type inference rules? Are the following two expressions well-typed? What are the type inference rules?
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1+card({TRUE}) 1+card({TRUE})
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{TRUE} ∪ {1} {TRUE} ∪ {1}
``` ```
%% Output %% Output
de.prob.exception.CliError: Exception while processing command result de.prob.exception.CliError: Exception while processing command result
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Inferenzregeln für Typen ### Inferenzregeln für Typen
Folgende Regeln sind relevant um die Typen der beiden Ausdrücke oben zu prüfen: Folgende Regeln sind relevant um die Typen der beiden Ausdrücke oben zu prüfen:
* type(1) = INTEGER * type(1) = INTEGER
* type(TRUE) = BOOL * type(TRUE) = BOOL
* type({ x }) = POW(XT) where type(x) = XT * type({ x }) = POW(XT) where type(x) = XT
* type(a+b) = INTEGER if type(a)=type(b)=INTEGER * type(a+b) = INTEGER if type(a)=type(b)=INTEGER
* type(a ∪ b) = POW(T) if type(a) = type(b) = POW(T) * type(a ∪ b) = POW(T) if type(a) = type(b) = POW(T)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Kleine Beispiele # Kleine Beispiele
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1+x=3 1+x=3
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 2$ * $\mathit{x} = 2$
TRUE TRUE
Solution: Solution:
x = 2 x = 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:language event_b :language event_b
``` ```
%% Output %% Output
Changed language for user input to Event-B (forced) Changed language for user input to Event-B (forced)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wenn man die Menge der Primzahlen so definiert, behält ProB diese als symbolische Menge: Wenn man die Menge der Primzahlen so definiert, behält ProB diese als symbolische Menge:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
``` ```
%% Output %% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$ $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$ * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
TRUE TRUE
Solution: Solution:
Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)} Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann aber zum Beispiel eine Primzahl generieren: Man kann aber zum Beispiel eine Primzahl generieren:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x∈Primzahlen ∧ Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} x∈Primzahlen ∧ Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
``` ```
%% Output %% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$ $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 2$ * $\mathit{x} = 2$
* $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$ * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
TRUE TRUE
Solution: Solution:
x = 2 x = 2
Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)} Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann die Menge der Primzahlen auch mit 1..100 schneiden um die Primzahlen bis 100 zu bekommen: Man kann die Menge der Primzahlen auch mit 1..100 schneiden um die Primzahlen bis 100 zu bekommen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧ Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧
res = Primzahlen ∩ 1..100 res = Primzahlen ∩ 1..100
``` ```
%% Output %% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$ $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{res} = \{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\}$ * $\mathit{res} = \{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\}$
* $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$ * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
TRUE TRUE
Solution: Solution:
res = {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} res = {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}
Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)} Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Hier rechnen wir jetzt die Anzahl der Primzahle bis 1000 aus: Hier rechnen wir jetzt die Anzahl der Primzahle bis 1000 aus:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧ Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧
res = card(Primzahlen ∩ 1..1000) res = card(Primzahlen ∩ 1..1000)
``` ```
%% Output %% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$ $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{res} = 168$ * $\mathit{res} = 168$
* $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$ * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
TRUE TRUE
Solution: Solution:
res = 168 res = 168
Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)} Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {x|x:1..20 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} :table {x|x:1..20 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
``` ```
%% Output %% Output
|x| |x|
|---| |---|
|1| |1|
|2| |2|
|3| |3|
|5| |5|
|7| |7|
|11| |11|
|13| |13|
|17| |17|
|19| |19|
x x
1 1
2 2
3 3
5 5
7 7
11 11
13 13
17 17
19 19
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......