Global snapshots 4

Zjemnenie pôvodnej špecifikácie:

• pre kazdý stav výpoctu (pôvodného programu) definujeme

  x.partial = x.rec if x.done ~
  
  x if ?x.done

• invariant a progress podmienka:

  invariant begun ? ? ?u, v: v obsahuje len zaznamenané premenné:: [init] u [partial] ? [partial] v [cur] ?
  
  begun ? ? ?x:: x.done ?

• neformálne:

  • partial je kombináciou rec a cur
    • pre zaznamenané rec = partial
    • pre nezaznamenané cur = partial
  • ked sa inicializuje zaznamenávanie, init = partial
  • ked sa zaznamenávanie skoncí, rec = partial
  • zaznamenávanie nemení partial
  • v necháva partial nezmenený

• Výpocet pre program EG

Previous slide

Next slide

Back to first slide

View graphic version