• English only

# Lab for Automated Reasoning and Analysis LARA

This is an old revision of the document!

# Hoare Logic

Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler.

## Example Proof

//{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}

## Hoare Triple for Sets and Relations

When (sets of states) and (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 precondition and 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 denotes one quadrant in plane, whereas a weaker condition denotes the entire half-plane.)

## Strongest Postcondition - sp

Definition: for , , $ sp(P,r) = \{ s' \mid \exists s. s \in P \land (s,s') \in r \}$

This is simply relation image of a set. (See Relation Image.)

### Lemma: Characterization of sp is the the smallest set such that , that is:

1. 2. ## Weakest Precondition - wp

Definition: for , , $ 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 when relation is non-deterministic.

### Lemma: Characterization of wp is the largest set such that , that is:

1. 2. ## 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 corresponds to doing 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:

• • • ## Hoare Triples, Preconditions, Postconditions on Formulas and Commands

Let and be formulas in our language (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 and execute , we obtain a state satisfying .

We then similarly extend the notion of and 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 sav08/hoare_logic.1236160985.txt.gz · Last modified: 2009/03/04 11:03 by vkuncak

© EPFL 2018 - Legal notice 