Vecerajúci filozofi: Spec1
Prvé priblízenie k riešeniu: Spec1
Spec1: (odn1), (odn2), (odn3), (odn4), kde
- invariant ?(u.e ? v.e ? E[u, v]) (odn3)
- (dn1), (dn3)?(dn5), ??u :: u.e ? ?u.e? /
/ ??u :: u.h ? u.e? (odn4)
musíme ukázat, ze
- user ? os splna (dn1), (dn2)
- os splna odmedzenia (odn1), (odn2)
Dôkaz:
- (dn3) ? (dn5) platí, lebo (odn1), (odn2) platí v os a (udn1) ? (udn3) platí pre user
- ?(u.e ? v.e ? E[u, v]) je stable in user lebo ?u.e aj ?v.e sú stable in user a E[u, v] je constant
- (dn1) platí v user ? os z predchádzajúceho a z (odn3) v os
- ??u :: u.e ? ?u.e? platí v user ? os lebo toto je dôsledok (udn4) a hypotézy (udn4) ? (dn1) platí v user ? os
- ??u :: u.h ? u.e? platí v user ? os, lebo je to dôsledok (odn4) a predpoklad (odn4) platí
- (dn1) platí v user ? os z predchádzajúceho