Pr-1st-1.1-m10-Slajd45

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

${𝒳}[{\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 >>