Is the following Hoare triple valid — i.e., the claimed relation between P, c, and Q is true?
    {{True}X ::= 5 {{X = 5}}
(1) Yes
(2) No

What about this one?
   {{X = 2}X ::= X + 1 {{X = 3}}
(1) Yes
(2) No

What about this one?
   {{True}X ::= 5; Y ::= 0 {{X = 5}}
(1) Yes
(2) No

What about this one?
   {{X = 2  X = 3}X ::= 5 {{X = 0}}
(1) Yes
(2) No

What about this one?
   {{True}SKIP {{False}}
(1) Yes
(2) No

What about this one?
   {{False}SKIP {{True}}
(1) Yes
(2) No

What about this one?
   {{True}WHILE True DO SKIP END {{False}}
(1) Yes
(2) No

What about this one?
    {{X = 0}}
    WHILE X == 0 DO X ::= X + 1 END
    {{X = 1}}
(1) Yes
(2) No

What about this one?
    {{X = 1}}
    WHILE X ≠ 0 DO X ::= X + 1 END
    {{X = 100}}
(1) Yes
(2) No

Proof Rules

Plan:
  • introduce one "proof rule" for each Imp syntactic form
  • plus a couple of a "structural rule" that helps glue proofs together
  • prove programs correct using these proof rules, without ever unfolding the definition of hoare

Assignment

The rule for assignment is the most fundamental of the Hoare logic proof rules. Here's how it works.
Consider this (valid) Hoare triple:
       {Y = 1 }}  X ::= Y  {X = 1 }}
In English: if we start out in a state where the value of Y is 1 and we assign Y to X, then we'll finish in a state where X is 1. That is, the property of being equal to 1 gets transferred from Y to X.
Similarly, in
       {Y + Z = 1 }}  X ::= Y + Z  {X = 1 }}
the same property (being equal to one) gets transferred to X from the expression Y + Z on the right-hand side of the assignment.
More generally, if a is any arithmetic expression, then
       {a = 1 }}  X ::= a {X = 1 }}
is a valid Hoare triple.
This can be made even more general. To conclude that an arbitrary property Q holds after X ::= a, we need to assume that Q holds before X ::= a, but with all occurrences of X replaced by a in Q. This leads to the Hoare rule for assignment
      {Q [X  a}X ::= a {Q }}
where "Q [X a]" is pronounced "Q where a is substituted for X".
For example, these are valid applications of the assignment rule:
      {{ (X ≤ 5) [X  X + 1]
         i.e., X + 1 ≤ 5 }}  
      X ::= X + 1  
      {X ≤ 5 }}

      {{ (X = 3) [X  3]
         i.e., 3 = 3}}  
      X ::= 3  
      {X = 3 }}

      {{ (0 ≤ X  X ≤ 5) [X  3]
         i.e., (0 ≤ 3  3 ≤ 5)}}  
      X ::= 3  
      {{ 0 ≤ X  X ≤ 5 }}
Now we can give the precise proof rule for assignment:
   (hoare_assign)  

{{Q [X  a]}} X ::= a {{Q}}

Consequence

Sometimes the preconditions and postconditions we get from the Hoare rules won't quite be the ones we want in the particular situation at hand — they may be logically equivalent but have a different syntactic form that fails to unify with the goal we are trying to prove, or they actually may be logically weaker (for preconditions) or stronger (for postconditions) than what we need.
For instance, while
      {{(X = 3) [X  3]}X ::= 3 {{X = 3}},
follows directly from the assignment rule,
      {{True}X ::= 3 {{X = 3}}.
does not. This triple is valid, but it is not an instance of hoare_assign because True and (X = 3) [X 3] are not syntactically equal assertions. However, they are logically equivalent, so if one triple is valid, then the other must certainly be as well. We might capture this observation with the following rule:
{{P'}} c {{Q}}
 P' (hoare_consequence_pre_equiv)  

{{P}} c {{Q}}
Taking this line of thought a bit further, we can see that strengthening the precondition or weakening the postcondition of a valid triple always produces another valid triple. This observation is captured by two Rules of Consequence.
{{P'}} c {{Q}}
 P' (hoare_consequence_pre)  

{{P}} c {{Q}}
{{P}} c {{Q'}}
Q'  Q (hoare_consequence_post)  

{{P}} c {{Q}}
For example, we might use the first consequence rule like this:
                {True }
                {{ 1 = 1 }
    X ::= 1
                {X = 1 }}

Finally, for convenience in some proofs, we can state a "combined" rule of consequence that allows us to vary both the precondition and the postcondition.
{{P'}} c {{Q'}}
 P'
Q'  Q (hoare_consequence)  

{{P}} c {{Q}}

Skip

Since SKIP doesn't change the state, it preserves any property P:
   (hoare_skip)  

{{ P }} SKIP {{ P }}

Sequencing

More interestingly, if the command c1 takes any state where P holds to a state where Q holds, and if c2 takes any state where Q holds to one where R holds, then doing c1 followed by c2 will take any state where P holds to one where R holds:
{{ P }} c1 {{ Q }}
{{ Q }} c2 {{ R }} (hoare_seq)  

{{ P }} c1;;c2 {{ R }}

Theorem hoare_seq : P Q R c1 c2,
     {{Q}} c2 {{R}}
     {{P}} c1 {{Q}}
     {{P}} c1;;c2 {{R}}.

Informally, a nice way of recording a proof using the sequencing rule is as a "decorated program" where the intermediate assertion Q is written between c1 and c2:
      {a = n }}
    X ::= a;;
      {X = n }}      <---- decoration for Q
    SKIP
      {X = n }}

Conditionals

What sort of rule do we want for reasoning about conditional commands? Certainly, if the same assertion Q holds after executing either branch, then it holds after the whole conditional. So we might be tempted to write:
{{P}} c1 {{Q}}
{{P}} c2 {{Q}}  

{{P}} IFB b THEN c1 ELSE c2 {{Q}}
However, this is rather weak. For example, using this rule, we cannot show that:
     {True }
     IFB X == 0
     THEN Y ::= 2
     ELSE Y ::= X + 1 
     FI
     {X ≤ Y }}
since the rule tells us nothing about the state in which the assignments take place in the "then" and "else" branches.
Better:
{{P   b}} c1 {{Q}}
{{P  ~b}} c2 {{Q}} (hoare_if)  

{{P}} IFB b THEN c1 ELSE c2 FI {{Q}}

Hoare Logic: So Far

Idea: create a domain specific logic for reasoning about properties of Imp programs.
  • This hides the low-level details of the semantics of the program
  • Leads to a compositional reasoning process
The basic structure is given by Hoare triples of the form:
  {{P}c {{Q}}
  • P and Q are predicates about the state of the Imp program
  • "If command c is started in a state satisfying assertion P, and if c eventually terminates in some final state, then this final state will satisfy the assertion Q."

Hoare Logic Rules (so far)

   (hoare_assign)  

{{Q [X  a]}} X::=a {{Q}}
   (hoare_skip)  

{{ P }} SKIP {{ P }}
{{ P }} c1 {{ Q }}
{{ Q }} c2 {{ R }} (hoare_seq)  

{{ P }} c1;;c2 {{ R }}
{{P   b}} c1 {{Q}}
{{P  ~b}} c2 {{Q}} (hoare_if)  

{{P}} IFB b THEN c1 ELSE c2 FI {{Q}}
{{P'}} c {{Q'}}
 P'
Q'  Q (hoare_consequence)  

{{P}} c {{Q}}

Example


    {{fun stTrue}}
  IFB (BEq (AVar X) (AInt 0))
    THEN (Y ::= (AInt 2))
    ELSE (Y ::= APlus (AVar X) (AInt 1))
  FI
    {{fun stst Xst Y}}.

Loops

Suppose we have a loop
      WHILE b DO c END
and we want to find a pre-condition P and a post-condition Q such that
      {{P}WHILE b DO c END {{Q}
is a valid triple.

If b is false, then the loop is like SKIP:
      {{P}WHILE b DO c END {{P}}.
But, as with if, we also know ¬b in the postcondition:
      {{P}WHILE b DO c END {{P  ¬b}}

What about when b is true?
First attempt:
{{P}} c {{P}}  

{{P}} WHILE b DO c END {{P  ~b}}

We know that b is true in the precondition of c
{{P  b}} c {{P}} (hoare_while)  

{{P}} WHILE b DO c END {{P  ~b}}
The proposition P is called an invariant of the loop.

One subtlety in the terminology is that calling some assertion P a "loop invariant" doesn't just mean that it is preserved by the body of the loop in question (i.e., {{P}} c {{P}}, where c is the loop body), but rather that P together with the fact that the loop's guard is true is a sufficient precondition for c to ensure P as a postcondition.
This is a slightly (but significantly) weaker requirement. For example, if P is the assertion X = 0, then P is an invariant of the loop
    WHILE X = 2 DO X := 1 END
although it is clearly not preserved by the body of the loop.

Is the assertion
    X = 0
an invariant of the following loop?
    WHILE X<100 DO X ::= X+1 END
(1) Yes
(2) No

Is the assertion
    Y = 0
an invariant of the following loop?
    WHILE X<100 DO X ::= X+1 END
(1) Yes
(2) No

Is the assertion
    X > 0
an invariant of the following loop?
    WHILE X = 0 DO X ::= X+1 END
(1) Yes
(2) No

Is the assertion
    X < 100
an invariant of the following loop?
    WHILE X<100 DO X ::= X+1 END
(1) Yes
(2) No

Is the assertion
    X > 10
an invariant of the following loop?
    WHILE X>10 DO X ::= X+1 END
(1) Yes
(2) No

Is the assertion
    X = Y + Z
an invariant of the following loop?
    WHILE Y>10 DO Y := Y-1; Z ::= Z+1 END
(1) Yes
(2) No

We can use the while rule to prove the following Hoare triple, which may seem surprising at first...

P Q,
  {{P}} WHILE BTrue DO SKIP END {{Q}}.

Complete List of Hoare Logic Rules

The rules of Hoare Logic:
   (hoare_assign)  

{{Q [X  a]}} X::=a {{Q}}
   (hoare_skip)  

{{ P }} SKIP {{ P }}
{{ P }} c1 {{ Q }}
{{ Q }} c2 {{ R }} (hoare_seq)  

{{ P }} c1;;c2 {{ R }}
{{P   b}} c1 {{Q}}
{{P  ~b}} c2 {{Q}} (hoare_if)  

{{P}} IFB b THEN c1 ELSE c2 FI {{Q}}
{{P  b}} c {{P}} (hoare_while)  

{{P}} WHILE b DO c END {{P  ~b}}
{{P'}} c {{Q'}}
 P'
Q'  Q (hoare_consequence)  

{{P}} c {{Q}}
In the next chapter, we'll see how these rules are used to prove that programs satisfy specifications of their behavior.