Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:hoare_logic [2009/03/04 11:03]
vkuncak
sav08:hoare_logic [2015/04/21 17:30] (current)
Line 28: 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 46: 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*}
  
-This is simply ​relation image of a set. (See [[Sets and relations#​Relation Image]].)+This is simply [[Sets and relations#​Relation Image]] ​of a set.
  
 {{sav08:​sp.png?​400x250|}} {{sav08:​sp.png?​400x250|}}
Line 65: 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 86: 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 134: 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 149: 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 
 
sav08/hoare_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice