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] (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