Pr-1st-1.1-m07-Slajd37

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Dowód poprawności koncepcji

Dowód poprawności koncepcji


Łatwo jest dowieść poprawności przedstawionej koncepcji konstrukcji obrazu spójnego. Skonstruowany obraz reprezentuje stan globalny, który wystąpił w chwili . Argumentując poprawność bardziej formalnie, zauważmy, że wyznaczony obraz uwzględnia wszystkie zdarzenia lokalne, które zaszły przed chwilą . Stąd,

gdzie jest czasem rzeczywistym zajścia zdarzenia .

Ponieważ zegar czasu rzeczywistego spełnia warunek poprawności zegara

,

otrzymujemy

a to właśnie należało wykazać.


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