Programová logika, invarianty, dokazování

Hoareova trojice

$$\begin{array}{c}\{x=0\}\\ x=x+1\\ \{x=1\}\end{array}$$

• obecně $\{something\}$ je výrok o stavu programu a uprostřed je program P
• prekondice … výrok o stavu programu před jeho začátkem $\{\varphi \}$
• postkondice … výrok o stavu programu po jeho konci $\{\psi \}$

Info

Pravdivost trojice je dána tak, že program je ve stavu spňujícím $\{\varphi \}$, poté se program $P$ vykoná a výsledný stav splňuje $\{\psi \}$.

(Axiom) přiřazení

$$\begin{array}{c}\{\varphi (v/e)\}\\ v=e\\ \{\psi \}\end{array}$$

• $v$ … proměnná
• $e$ … výraz
• $\varphi$ … tvrzení
• $\varphi (v/e)$ … nahrazení $v$ za $e$ ve $\varphi$
• Např.

$$\begin{array}{c}\{x+1=2\}\\ x\leftarrow x+1\\ \{x=2\}\end{array}$$

- *A to dále můžeme zjednodušit jako*

$$\begin{array}{c}\{x=1\}\\ x\leftarrow x+1\\ \{x=2\}\end{array}$$

• Můžeme zesílit prekondici a oslabit postkondici

Nenarušení tvrzení

• $P$ … akce
• $\varphi$ … prekondice $P$
• $\psi$ … tvrzení
• $\psi$ není narušeno (neinterferuje s) $P$ jestliže:

\{ψ∧ϕ\}\\ P\\ \{ψ\} \end{gather}

Info

Náčrtky důkazů se nemohou narušit pokud mají disjunktní proměnné.

• invariant programu … tvrzení, které platí v každém stavu jeho historie (neboli platí na počátku a nikde v průběhu není narušeno)