Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:hoare_logic [2009/03/04 11:03]
vkuncak
sav08:hoare_logic [2015/04/21 17:30]
Line 1: Line 1:
-====== Hoare Logic ====== 
  
-Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler. 
- 
- 
-===== Example Proof ===== 
- 
-<code java> 
-//{0 <= y} 
-i = y; 
-//{0 <= y & i = y} 
-r = 0; 
-//{0 <= y & i = y & r = 0} 
-while //{r = (y-i)*x & 0 <= i} 
- (i > 0) ( 
-  //{r = (y-i)*x & 0 < i} 
-  r = r + x; 
-  //{r = (y-i+1)*x & 0 < i} 
-  i = i - 1 
-  //{r = (y-i)*x & 0 <= i} 
-) 
-//{r = x * y} 
-</​code>​ 
- 
- 
-===== Hoare Triple for Sets and Relations ===== 
- 
-When $P, Q \subseteq S$ (sets of states) and $r \subseteq S\times S$ (relation on states, command semantics) then 
-Hoare triple 
-\[ 
-    \{P \}\ r\ \{ Q \} 
-\] 
-means 
-\[ 
-    \forall s,s' \in S. s \in P \land (s,s') \in r \rightarrow s' \in Q 
-\] 
-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.) 
- 
- 
- 
- 
- 
-===== Strongest Postcondition - sp ===== 
- 
-Definition: for $P \subseteq S$, $r \subseteq S\times S$, 
-\[ 
-   ​sp(P,​r) = \{ s' \mid \exists s. s \in P \land (s,s') \in r \} 
-\] 
- 
-This is simply relation image of a set. (See [[Sets and relations#​Relation Image]].) 
- 
-{{sav08:​sp.png?​400x250|}} 
- 
- 
-==== Lemma: Characterization of sp ==== 
- 
-$sp(P,r)$ is the the smallest set $Q$ such that $\{P\}r\{Q\}$,​ that is: 
-  - $\{P\} r \{ sp(P,r) \}$ 
-  - $\forall Q \subseteq S.\ \{P\} r \{Q\} \rightarrow sp(P,r) \subseteq Q$ 
- 
- 
-===== Weakest Precondition - wp ===== 
- 
-Definition: for $Q \subseteq S$, $r \subseteq S \times S$, 
-\[ 
-   ​wp(r,​Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \} 
-\] 
- 
-Note that this is in general not the same as $sp(Q,​r^{-1})$ when relation is non-deterministic. 
- 
-{{sav08:​wp.png?​400x250|}} 
- 
-==== Lemma: Characterization of wp ==== 
- 
-$wp(r,Q)$ is the largest set $P$ such that $\{P\}r\{Q\}$,​ that is: 
-  - $\{wp(r,​Q)\} r \{Q \}$ 
-  - $\forall P \subseteq S.\ \{P\} r \{Q\} \rightarrow P \subseteq wp(r,Q)$ 
- 
-===== Some More Laws on Preconditions and Postconditions ===== 
- 
-We next list several more lemmas on properties of wp, sp, and Hoare triples. 
- 
-==== Postcondition of inverse versus wp ==== 
- 
-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: 
-\[ 
-    S \setminus wp(r,Q) = sp(S \setminus Q,r^{-1}) 
-\] 
- 
-==== Disjunctivity of sp ==== 
- 
-\[ 
-   ​sp(P_1 \cup P_2,r) = sp(P_1,r) \cup sp(P_2,r) 
-\] 
-\[ 
-   ​sp(P,​r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2) 
-\] 
- 
-==== Conjunctivity of wp ==== 
- 
-\[ 
-    wp(r,Q_1 \cap Q_2) = wp(r,Q_1) \cap wp(r,Q_2) 
-\] 
- 
-\[ 
-    wp(r_1 \cup r_2,Q) = wp(r_1,Q) \cap wp(r_2,Q) 
-\] 
- 
-==== Pointwise wp ===== 
- 
-\[ 
-    wp(r,Q) = \{ s \mid s \in S \land sp(\{s\},r) \subseteq Q \} 
-\] 
- 
-==== Pointwise sp ===== 
- 
-\[ 
-   ​sp(P,​r) = \bigcup_{s \in P} sp(\{s\},​r) ​ 
-\] 
- 
-==== Three Forms of Hoare Triple ==== 
- 
-The following three conditions are equivalent: 
-  * $\{P\} r \{Q\}$ 
- 
-  * $P \subseteq wp(r,Q)$ 
- 
-  * $sp(P,r) \subseteq Q$ 
- 
- 
-===== Hoare Triples, Preconditions,​ Postconditions on Formulas and Commands ===== 
- 
-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: 
-\[ 
-   \{ P \} c \{ Q \}    ​ 
-\] 
-means 
-\[ 
-    \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) 
-\] 
-In words: if we start in a state satisfying $P$ and execute $c$, we obtain a state satisfying $Q$.  ​ 
- 
-We then similarly extend the notion of $sp(P,r)$ and $wp(r,Q)$ to work on formulas and commands. ​  We use the same notation and infer from the context whether we are dealing with sets and relations or formulas and commands. 
- 
- 
- 
-===== Composing Hoare Triples ===== 
- 
-\[ 
-\frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} } 
-     { \{P\} c_1 ; c_2 \{ R \} } 
-\] 
- 
-We can prove this from  
-  * definition of Hoare triple ​ 
-  * meaning of ';'​ as $\circ$ 
- 
-===== Further reading ===== 
- 
-  * {{sav08:​backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}} 
 
sav08/hoare_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice