Pr-1st-1.1-m10-Slajd45

Algorytm detekcji zakończenia statycznego: Dowód poprawności - oznaczenia (2)

${\mathcal {X}}[\tau _{i}^{k}]$ - jest wartością zmiennej (predykatu) w chwili $\tau _{i}^{k}$

$Q_{\alpha }$ - dla ułatwienia zostanie przyjęte, że inicjator jest dodatkowym procesem, nie związanym z procesami aplikacyjnymi.

<< Poprzedni slajd | Spis treści | Następny slajd >>