Hoare Tripple

A Hoare tripple is a statement $\langle \alpha \rangle \; P \; \langle \beta \rangle$ where $\alpha,\beta$ are tests on the state space $X$ and $P$ a program (= piece of code) acting on $X$. We say the tripple is partially correct if, whenever $\underline{x} \in X$   satisfies$\alpha$, and $P$ is applied to $x$, the result (if it exists) satisfies $\beta$. It is totally correct if any input $x$ satisfying $\alpha$ does give a result when $P$ is applied ($P$ terminates on $x$), and this result satisfies $\beta$.

Recalling the factorial program $P$, it appears that $\langle n \geq 1 \rangle \; P \; \langle P = n! \rangle$ is both partially and totally correct. Note taht neither $(n \geq 1)$ nor $(p = n!)$ involves the varible ``i'', so its value is not relevant to the correctness.

We call the $\alpha,\beta$ in $\langle \alpha \rangle \; P \; \langle \beta \rangle$ the precondition and postcondition respectively.