Faulty channels 5

• Správnost P2:

  invariant mr ? ms
  
  |mr| = n ? |mr| = n + 1

• Pozorovanie: (I1) platí aj pre P2, kde miesto x je x.dex

• oznacenie x.val ? ms ak ?j : x.val = ms[j]

• platí nasledovný

  invariant x.val ? ms ? mr ? ms ? |mr| = kr (I2)
  

(Hint: z (I1) kr ? x.dex ? kr + 1 = x.dex)

• Progress podmienka má podobný dôkaz ako v P1

• Poznámka. Z (I1) a hintu kr := x.dex if kr ? x.dex mozno v P2 nahradit kr := kr + 1 if kr ? x.dex a zároven mozno kr := y + 1 nahradit ks := ks + 1 if ks = y

Previous slide

Next slide

Back to first slide

View graphic version