Pr-1st-1.1-m07-Slajd37

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 ${\tau }_s$. Argumentując poprawność bardziej formalnie, zauważmy, że wyznaczony obraz uwzględnia wszystkie zdarzenia lokalne, które zaszły przed chwilą ${\tau }_s$. Stąd,

$(E^{\prime }\in H_i({\tau }_s)\wedge {ℛ}{𝒯}(E)<{ℛ}{𝒯}(E^{\prime }))\Rightarrow (E\in H_i({\tau }_s))$

gdzie ${ℛ}{𝒯}(E)$ jest czasem rzeczywistym zajścia zdarzenia $E$.

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

$(E\mapsto E^{\prime })\Rightarrow {ℛ}{𝒯}(E)<{ℛ}{𝒯}(E^{\prime })$,

otrzymujemy

$(E^{\prime }\in H_i({\tau }_s)\wedge E\mapsto E^{\prime })\Rightarrow (E\in H_i({\tau }_s))$

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

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