Byzantská dohoda: Spec4
Vlastnosti (B1) a (B2) sa uz lahko implementujú ako rovnice. (E1) ? (E5) uz sú priamo rovnice, teraz ostáva prepísat (A3) do rovníc.
robsr[u, z, x]? lokálna k u, ktorá cíta hodnotu obsr[z, x]
sumr[u, x] ? pocet z takých, ze je robsr[u, z, x] true
Spec4: (B1), (B2), (E1) ? (E5) a nasledujúce:
(E6) robsr[u, z, x] = obsr[z, x]
(E7) sumr[u, x] = ? +z: robsr[u, z, x]:: 1 ?
Vysvetlenie:
- proces u cíta pocet procesov z, pre ktoré platí obsr[z, x]; výsledok si ulozí do sumr[u, x]
- zapocítajú sa všetky spolahlivé w, pre ktoré platí
obsr[w, x], a teda platí dolná hranica
- kedze máme t nespolahlivých, hodnota sumr[u, x] nemôze prekrocit ? +w: obsr[w, x]:: 1 ? o viac nez t
Tým je dokázaná správnost Spec4 (lebo Spec4 ? Spec3).