Programming Logic
{p} S {q} if S terminates
p: precondition, q: postcondition, S: statement
predikáty nie sú viazané s nejakými miestami v programe, ako u sekvencných programov
logika pre uvazovanie o nekonecných postupnostiach programových stavov
tvrdenie {true} t {p} (pre príkaz t programu F) hovorí, ze niekedy raz (eventually) p bude platit
budeme predpokladat, ze program má aspon jeden príkaz
viacero výrokov v hypotéze znamená konjukciu
viacero výrokov v závere znamená disjukciu
Basic Concepts: (hypotéza / záver)
- {p} S {true}
- {false} S {q}
- {p} S {false} / R p
- {p} S {q}, {p’} S {q’} / {p Ú p’} S {q Ú q’}
- {p} S {q}, {p’} S {q’} / {p Ú p’} S {q Ú q’}
- p’ T p, {p} S {q}, q T q’ / {p’} S {q’}