|[ con N: int; {N≥0}
var f: array[0..N) of int; t:array[0..N) of bool;
n:int;
n:=0;
{P0∧P1}
do n < N →
f.n:=rand(100);
n:=n+1
{P0∧P1}
od
{∀j: 0≤j<N: 0≤f.j<100}
n:=0;
{P2∧P1}
do n < N →
t.n:=f.n>40;
n:=n+1
{P2∧P1}
od
{∀j: 0≤j<N: t.j=f.j>40}
]|

PO: {∀j: 0≤j<n: 0≤f.j<100}
P1: O ≤ n ≤ N
P2: {∀j: 0≤j<n: t.j=f.j>40}
O≤round(K)<K ∧ K>0