Faulty channels 4
dokázeme progress podmienku
kr = n ? y = n ? ks = n + 1 ? y = n + 1 ? kr = n + 1
Dôkaz: ukázeme pre y = n ? ks = n + 1, ostatné podobne
- y = n ensures ks = n + 1 vyplýva z nasledovného:
- y = n ? ks ? n + 1 ? y = kr = x = ks {z (I1)}
- {y = n} ks := y + 1 {ks = n + 1}
- {y = n ? ks ? n + 1} s {y = n ? ks = n + 1}
Prenos lubovolnej postupnosti dát
ms – nekonecná postupnost (lokálna senderu)
mr – nekonecná postupnost (lokálna receiveru)
ms[j], j > 0 oznacuje j-ty element ms
do x sa píše dvojica x.dex, x.val
Program P2
declare x: (integer, data item), y, ks, kr: integer
initially y, ks, kr = 0, 1, 0 ? mr = null ? x = (1, ms[1])
assign
y := kr {receiver}
? ks := y + 1 {sender}
? x := (ks, ms[ks]) {sender}
? kr, mr := x.dex, mr ; x.val if kr ? x.dex {receiver}