Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:hoare_logic [2009/02/25 14:35] vkuncak |
sav08:hoare_logic [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 2: | Line 2: | ||
Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler. | Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler. | ||
+ | |||
===== Example Proof ===== | ===== Example Proof ===== | ||
- | <code> | + | <code java> |
- | {0 <= y} | + | //{0 <= y} |
i = y; | i = y; | ||
- | {0 <= y & i = y} | + | //{0 <= y & i = y} |
r = 0; | r = 0; | ||
- | {0 <= y & i = y & r = 0} | + | //{0 <= y & i = y & r = 0} |
- | while {r = (y-i)*x & 0 <= i} | + | while //{r = (y-i)*x & 0 <= i} |
(i > 0) ( | (i > 0) ( | ||
- | {r = (y-i)*x & 0 < i} | + | //{r = (y-i)*x & 0 < i} |
r = r + x; | r = r + x; | ||
- | {r = (y-i+1)*x & 0 < i} | + | //{r = (y-i+1)*x & 0 < i} |
i = i - 1 | i = i - 1 | ||
- | {r = (y-i)*x & 0 <= i} | + | //{r = (y-i)*x & 0 <= i} |
) | ) | ||
- | {r = x * y} | + | //{r = x * y} |
</code> | </code> | ||
Line 27: | Line 28: | ||
When $P, Q \subseteq S$ (sets of states) and $r \subseteq S\times S$ (relation on states, command semantics) then | When $P, Q \subseteq S$ (sets of states) and $r \subseteq S\times S$ (relation on states, command semantics) then | ||
Hoare triple | Hoare triple | ||
- | \[ | + | \begin{equation*} |
\{P \}\ r\ \{ Q \} | \{P \}\ r\ \{ Q \} | ||
- | \] | + | \end{equation*} |
means | means | ||
- | \[ | + | \begin{equation*} |
\forall s,s' \in S. s \in P \land (s,s') \in r \rightarrow s' \in Q | \forall s,s' \in S. s \in P \land (s,s') \in r \rightarrow s' \in Q | ||
- | \] | + | \end{equation*} |
We call $P$ precondition and $Q$ postcondition. | We call $P$ precondition and $Q$ postcondition. | ||
Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically, a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas a weaker condition $x > 0$ denotes the entire half-plane.) | Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically, a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas a weaker condition $x > 0$ denotes the entire half-plane.) | ||
+ | |||
+ | |||
+ | |||
Line 43: | Line 47: | ||
Definition: for $P \subseteq S$, $r \subseteq S\times S$, | Definition: for $P \subseteq S$, $r \subseteq S\times S$, | ||
- | \[ | + | \begin{equation*} |
sp(P,r) = \{ s' \mid \exists s. s \in P \land (s,s') \in r \} | sp(P,r) = \{ s' \mid \exists s. s \in P \land (s,s') \in r \} | ||
- | \] | + | \end{equation*} |
- | Note the similarity with relation composition. | + | This is simply [[Sets and relations#Relation Image]] of a set. |
{{sav08:sp.png?400x250|}} | {{sav08:sp.png?400x250|}} | ||
Line 62: | Line 66: | ||
Definition: for $Q \subseteq S$, $r \subseteq S \times S$, | Definition: for $Q \subseteq S$, $r \subseteq S \times S$, | ||
- | \[ | + | \begin{equation*} |
wp(r,Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \} | wp(r,Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \} | ||
- | \] | + | \end{equation*} |
Note that this is in general not the same as $sp(Q,r^{-1})$ when relation is non-deterministic. | Note that this is in general not the same as $sp(Q,r^{-1})$ when relation is non-deterministic. | ||
Line 83: | Line 87: | ||
If instead of good states we look at the completement set of "error states", then $wp$ corresponds to doing $sp$ backwards. In other words, we have the following: | If instead of good states we look at the completement set of "error states", then $wp$ corresponds to doing $sp$ backwards. In other words, we have the following: | ||
- | \[ | + | \begin{equation*} |
S \setminus wp(r,Q) = sp(S \setminus Q,r^{-1}) | S \setminus wp(r,Q) = sp(S \setminus Q,r^{-1}) | ||
- | \] | + | \end{equation*} |
==== Disjunctivity of sp ==== | ==== Disjunctivity of sp ==== | ||
- | \[ | + | \begin{equation*} |
sp(P_1 \cup P_2,r) = sp(P_1,r) \cup sp(P_2,r) | sp(P_1 \cup P_2,r) = sp(P_1,r) \cup sp(P_2,r) | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
sp(P,r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2) | sp(P,r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2) | ||
- | \] | + | \end{equation*} |
==== Conjunctivity of wp ==== | ==== Conjunctivity of wp ==== | ||
- | \[ | + | \begin{equation*} |
wp(r,Q_1 \cap Q_2) = wp(r,Q_1) \cap wp(r,Q_2) | wp(r,Q_1 \cap Q_2) = wp(r,Q_1) \cap wp(r,Q_2) | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
wp(r_1 \cup r_2,Q) = wp(r_1,Q) \cap wp(r_2,Q) | wp(r_1 \cup r_2,Q) = wp(r_1,Q) \cap wp(r_2,Q) | ||
- | \] | + | \end{equation*} |
==== Pointwise wp ===== | ==== Pointwise wp ===== | ||
- | \[ | + | \begin{equation*} |
wp(r,Q) = \{ s \mid s \in S \land sp(\{s\},r) \subseteq Q \} | wp(r,Q) = \{ s \mid s \in S \land sp(\{s\},r) \subseteq Q \} | ||
- | \] | + | \end{equation*} |
==== Pointwise sp ===== | ==== Pointwise sp ===== | ||
- | \[ | + | \begin{equation*} |
sp(P,r) = \bigcup_{s \in P} sp(\{s\},r) | sp(P,r) = \bigcup_{s \in P} sp(\{s\},r) | ||
- | \] | + | \end{equation*} |
==== Three Forms of Hoare Triple ==== | ==== Three Forms of Hoare Triple ==== | ||
Line 131: | Line 135: | ||
Let $P$ and $Q$ be formulas in our language $F$ (see [[simple programming language]]). We define Hoare triples on these syntactic entities by taking their interpretation as sets and relations: | Let $P$ and $Q$ be formulas in our language $F$ (see [[simple programming language]]). We define Hoare triples on these syntactic entities by taking their interpretation as sets and relations: | ||
- | \[ | + | \begin{equation*} |
\{ P \} c \{ Q \} | \{ P \} c \{ Q \} | ||
- | \] | + | \end{equation*} |
means | means | ||
- | \[ | + | \begin{equation*} |
\forall s_1, s_2.\ f_T(P)(s_1) \land (s_1,s_2) \in r_c(c) \rightarrow f_T(Q)(s_1) | \forall s_1, s_2.\ f_T(P)(s_1) \land (s_1,s_2) \in r_c(c) \rightarrow f_T(Q)(s_1) | ||
- | \] | + | \end{equation*} |
In words: if we start in a state satisfying $P$ and execute $c$, we obtain a state satisfying $Q$. | In words: if we start in a state satisfying $P$ and execute $c$, we obtain a state satisfying $Q$. | ||
Line 146: | Line 150: | ||
===== Composing Hoare Triples ===== | ===== Composing Hoare Triples ===== | ||
- | \[ | + | \begin{equation*} |
\frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} } | \frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} } | ||
{ \{P\} c_1 ; c_2 \{ R \} } | { \{P\} c_1 ; c_2 \{ R \} } | ||
- | \] | + | \end{equation*} |
We can prove this from | We can prove this from |