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

add presentation

parent ee5acbfb
Branches
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
## Introduction to B ##
%% Cell type:markdown id: tags:
### Basic Datavalues ###
%% Cell type:markdown id: tags:
B provides the booleans, strings and integers as built-in datatypes.
%% Cell type:code id: tags:
``` prob
BOOL
```
%% Output
{FALSE,TRUE}
%% Cell type:code id: tags:
``` prob
"this is a string"
```
%% Output
"this is a string"
%% Cell type:code id: tags:
``` prob
1024
```
%% Output
1024
%% Cell type:markdown id: tags:
Users can define their own datatype in a B machine.
One distinguishes between explicitly specified enumerated sets and deferred sets.
%% Cell type:code id: tags:
``` prob
::load
MACHINE MyBasicSets
SETS Trains = {thomas, gordon}; Points
END
```
%% Output
[2018-05-25 13:12:41,869, T+1176691] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh
[2018-05-25 13:12:43,407, T+1178229] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54757
[2018-05-25 13:12:43,408, T+1178230] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 94534
[2018-05-25 13:12:43,412, T+1178234] "ProB Output Logger for instance 6e2e7ba7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-25 13:12:43,441, T+1178263] "ProB Output Logger for instance 6e2e7ba7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
Loaded machine: MyBasicSets : []
%% Cell type:markdown id: tags:
For animation and constraint solving purposes, ProB will instantiate deferred sets to some finite set (the size of which can be controlled).
%% Cell type:code id: tags:
``` prob
Points
```
%% Output
{Points1,Points2}
%% Cell type:markdown id: tags:
### Pairs ###
B also has pairs of values, which can be written in two ways:
%% Cell type:code id: tags:
``` prob
(thomas,10)
```
%% Output
(thomas↦10)
%% Cell type:code id: tags:
``` prob
thomas |-> 10
```
%% Output
(thomas↦10)
%% Cell type:markdown id: tags:
Tuples simply correspond to nested pairs:
%% Cell type:code id: tags:
``` prob
(thomas |-> gordon |-> 20)
```
%% Output
((thomas↦gordon)↦20)
%% Cell type:markdown id: tags:
### Sets ###
Sets in B can be specified in multiple ways.
For example, using explicit enumeration:
%% Cell type:code id: tags:
``` prob
{1,3,2,3}
```
%% Output
{1,2,3}
%% Cell type:markdown id: tags:
or via a predicate by using a set comprehension:
%% Cell type:code id: tags:
``` prob
{x|x>0 & x<4}
```
%% Output
{1,2,3}
%% Cell type:markdown id: tags:
For integers there are a variety of other sets, such as intervals:
%% Cell type:code id: tags:
``` prob
1..3
```
%% Output
{1,2,3}
%% Cell type:markdown id: tags:
or the set of implementable integers INT = MININT..MAXINT or the set of implementable natural numbers NAT = 0..MAXINT.
%% Cell type:markdown id: tags:
Sets can be higher-order and contain other sets:
%% Cell type:code id: tags:
``` prob
{ 1..3, {1,2,3,2}, 0..1, {x|x>0 & x<4} }
```
%% Output
{{0,1},{1,2,3}}
%% Cell type:markdown id: tags:
Relations are modelled as sets of pairs:
%% Cell type:code id: tags:
``` prob
{ thomas|->gordon, gordon|->gordon, thomas|->thomas}
```
%% Output
{(thomas↦thomas),(thomas↦gordon),(gordon↦gordon)}
%% Cell type:markdown id: tags:
Functions are relations which map every domain element to at most one value:
%% Cell type:code id: tags:
``` prob
{ thomas|->1, gordon|->2}
```
%% Output
{(thomas↦1),(gordon↦2)}
%% Cell type:markdown id: tags:
## Expressions vs Predicates vs Substitutions ##
%% Cell type:markdown id: tags:
### Expressions ###
Expressions in B have a value. With ProB and with ProB's Jupyter backend, you can evaluate expresssions such as:
%% Cell type:code id: tags:
``` prob
2**1000
```
%% Output
10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376
%% Cell type:markdown id: tags:
B provides many operators which return values, such as the usual arithmetic operators but also many operators for sets, relations and functions.
%% Cell type:code id: tags:
``` prob
(1..3 \/ 5..10) \ (2..6)
```
%% Output
{1,7,8,9,10}
%% Cell type:code id: tags:
``` prob
ran({(thomas↦1),(gordon↦2)})
```
%% Output
{1,2}
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)} (thomas)
```
%% Output
1
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)}~[2..3]
```
%% Output
{gordon}
%% Cell type:markdown id: tags:
## Predicates
ProB can also be used to evaluate predicates (B distinguishes between expressions which have a value and predicates which are either true or false).
%% Cell type:code id: tags:
``` prob
2>3
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
3>2
```
%% Output
TRUE
%% Cell type:markdown id: tags:
Within predicates you can use **open** variables, which are implicitly existentially quantified.
ProB will display the solution for the open variables, if possible.
%% Cell type:code id: tags:
``` prob
x*x=100
```
%% Output
TRUE
Solution:
x = −10
%% Cell type:markdown id: tags:
We can find all solutions to a predicate by using the set comprehension notation.
Note that by this we turn a predicate into an expression.
%% Cell type:code id: tags:
``` prob
{x|x*x=100}
```
%% Output
{−10,10}
%% Cell type:markdown id: tags:
### Substitutions ###
B also has a rich syntax for substitutions, aka statements.
For example ```x := x+1``` increments the value of x by 1.
We will not talk about substitutions in the rest of this presentation.
%% Cell type:code id: tags:
``` prob
```
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment