PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 1
guard
B: Boolean expression
S: command
B → S: guarded command
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 2
IF
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 3
Command IF can be executed as follows.
1. If any guard Bi is not well-defined in the state in
which execution begins, abortion may occur.
(This is because nothing is assumed about the order of
evaluation of the guards.)
2. At least one guard must be true; otherwise
execution aborts.
3. If at least one guard is true, then one guarded
command Bi → Si with true guard Bi is chosen
and Si is executed.
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 4
At least one guard must be true
The guards must be well-defined
Execution of each command Si
with a true guard Bi
terminates with R true
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 5
We assume that the guards are total functions – i.e. are well-defined
in all states.
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 6
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 7
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 8
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 9
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 10
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 11
$ python3 gries_10_4.py 20
b = [30, 10, -10, 50, -100, 20, 50, 50, -70, -90, 20, 60, -80, 60, -
80, 70, -50, -30, 40, 20]
i = 1
p = 1
Postcondition is established
$ python3 gries_10_4.py 20
b = [-10, 60, -10, 40, -50, 30, -80, -10, -30, -10, 80, -40, 80, -60,
80, -50, 30, 80, 30, 50]
i = 5
p = 2
Postcondition is established
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 12
$ python3 gries_10_4.py 20
b = [90, -70, 20, -70, 30, 100, 70, 80, 10, 40, -40, 20, -100, 0, -30,
-70, 100, 90, -80, 40]
i = 5
p = 3
Postcondition is established
Traceback (most recent call last):
File "gries_10_4.py", line 32, in <module>
assert b.count(0) == 0
AssertionError
$ python3 gries_10_4.py 20
b = [20, -40, -100, 0, 30, 50, 100, -40, 10, 80, -50, -80, 70, -80, -
30, 60, -10, -40, -20, -100]
i = 3
p = 1
Traceback (most recent call last):
File "gries_10_4.py", line 21, in <module>
'Precondition failed'
AssertionError: Precondition failed
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 13
Some comments about an alternative command
if (B1) S1;
if (B1) S1; else S2;
vs.
switch (B1)
{
case v1: S1; break;
case v2: S2; break;
…
default: Sn;
}
No defaults!
The possibility of nondeterminism!
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 14
$ cat -n max.pml | expand
1 /* Copyright 2007
2 by Moti Ben-Ari
3 under the GNU GPL */
4
5 active proctype P() { PROMELA language
6 int a = 5, b = 5
7 int max
8 int branch
9
10 if
11 :: a >= b -> max = a; branch = 1
12 :: b >= a -> max = b; branch = 2
13 fi
14 printf("The maximum of %d and %d = %d by branch %d\n",
15 a, b, max, branch)
16 }
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 15
$ spin max.pml
The maximum of 5 and 5 = 5 by branch 1
1 process created
$ spin max.pml
The maximum of 5 and 5 = 5 by branch 1
1 process created
$ spin max.pml
The maximum of 5 and 5 = 5 by branch 2
1 process created
$ spin max.pml
The maximum of 5 and 5 = 5 by branch 1
1 process created
$ spin max.pml
The maximum of 5 and 5 = 5 by branch 2
1 process created
$ spin max.pml
The maximum of 5 and 5 = 5 by branch 2
1 process created
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 16
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 17
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 18
$ python3 max_nondet_v1.py 5 7
max = 7 is from b, branch 2 (baab)
$ python3 max_nondet_v1.py 5 7
max = 7 is from b, branch 2 (abba)
$ python3 max_nondet_v1.py 15 7
max = 15 is from a, branch 1 (baab)
$ python3 max_nondet_v1.py 15 7
max = 15 is from a, branch 1 (abba)
$ python3 max_nondet_v1.py 17 17
max = 17 is from a, branch 1 (abba)
$ python3 max_nondet_v1.py 17 17
max = 17 is from b, branch 2 (baab)
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 19
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 20
$ python3 max_nondet_v2.py 23 14
The maximum of a(23) and b(14) = 23 by branch 1
$ python3 max_nondet_v2.py 23 37
The maximum of a(23) and b(37) = 37 by branch 2
$ python3 max_nondet_v2.py 44 44
The maximum of a(44) and b(44) = 44 by branch 1
$ python3 max_nondet_v2.py 44 44
The maximum of a(44) and b(44) = 44 by branch 2
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 21
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 22
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 23
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 24
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 25
0 i k j n
b x
0 i k j n
b x
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 26
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 27
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 28
$ python3 gries_10_6.py 100
b[0:99], i=16, k=29, b[k]=386, j=49, m=46, x=557
b[0:99], i=29, k=29, b[k]=386, j=49, m=46, x=557
$ python3 gries_10_6.py 100
b[0:99], i=63, k=74, b[k]=760, j=93, m=73, x=743
b[0:99], i=63, k=74, b[k]=760, j=74, m=73, x=743
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 29
PUCP, 2020, vk 1INF06 Estructura de Datos y Programación Metódica 30
