Method by Tony Hoare to verify that an imperative program is correct with respect to a given specification, i.e., reasoning about program correctness using pre and post conditions.

• Goal: to prove that a program S is correct with respect to a given precondition P and postcondition Q.
• Method:
  • Use Hoare tripple to represent S,P,Q and prove the tripple
  • Compute weakest precondition of S with respect to Q, i.e., wp(S, Q)
  • For every loop in S, need to provide a loop invariant
  • Form verification condition (vc): P => wp(S, Q)
    • If this vc is true, then the Hoare tripple is valid, i.e., S is correct wrt to P and Q
    • Else, Hoare tripple is invalid but we cannot conclude that S is incorrect wrt to P and Q (e.g., it could be that we picked a weak loop invariant)

• S: a program (a list of statements); P: precondition (a formula that holds before the execution of S); Q: postcondition (a formula that holds after the execution of S)
• Read: assume P holds, if S executes successfully (i.e., terminates), then Q holds
• Meaning: if the tripple is [valid]{.underline}, then S is correct wrt to the program specification (P and Q)
• E.g., {x = 5 and y > 2} z := x + y; z := z + 2 {z > 9}: assume x=5 and y > 2, if z:x +y; z := z + 2 runs successfully, then we have z > 9

• Partial: assume P holds and S successfully executes, Q holds
  • Here, we assume P and the program terminates (S successfully executed)
• Total: assume P holds, if S successfully executes, then Q holds
  • Here, we require S terminates
  • Dififcult because having to ensure the termination of S
• We often just use partial correctness because total correctness requires us to also prove that S would terminate, which is a difficult problem (theoretically undecidable).

1. Consider a program S with a single assignment statement x:=5.

   The Hoare tripple {True} x := 5 {x > 6} is not a valid tripple, but these next ones are valid:

   1. {True} x := 5 {x=5 or x= 6 or x > 6}
   2. {True} x := 5 {x > 1}
   3. {True} x := 5 {x = 5}

   Moreover, the postcondition in x=5 is strongest because it is more precise than x > 1 and (x=5 or x=6 or x > 6). In general we want the strongest (most precise) postcondition.

2. Consider another program z:= x/y

   These are valid Hoare tripples:

   1. {x = 1 & y = 2} z:= x/y {z < 1}
   2. {x = 2 & y = 4} z:= x/y {z <1}
   3. {0 < x < y & y != 0} z:= x/y {z <1}

   Moreover, the precondition 0 < x < y & y != 0 is the weakest precondition (i.e., it is the least constraint precondition). In general we want the weakest precondition.

   These are invalid tripples:

   1. {x < y} z:= x/y {z < 1} (counterexample input x=-1, y=0, after executing z:=x/y, we do not have z < 1 and instead got a div-by-0 exception)
   2. {x = 0} z:= x/y {z < 1} (counterexample input x=0, y=0)
   3. {y != 0} z:= x/y {z < 1} (counterexample input x=2 , y=1)
   4. {x < y & y != 0} z:= x/y {z <1} (counterexample input x=-2, y=-1)

Fill in P,S,Q to make the following Hoare tripples valid.

1. {P} x:=3 {x = 8}

2. {P} x:= y - 3 {x = 8}

3. {x = y} S {x = y}

4. {x < 0} while(x!=0) do x := x - 1 {Q}

We can automatically verify (partial) program correctness using Hoare triples and weakest preconditions. To prove {P} S {Q} is valid, i.e., to prove the program S is correct wrt to the precondition P and postcondition Q, we form a verification condition P => wp(S, Q) and check that it is valid. Here, the function wp returns the weakest precondition (WP) allowing the program S to achieve the postcondition Q. Thus, to show the validity of {P} S {Q}, we show that P implies (=>) the WP of S wrt to Q.

Let's look at weakest preconditions. The function wp(S,Q) returns the weakest precondition (a logical formula) from a given program S, and a formula Q. wp is defined using the following rules for different kind of (imperative) program statements as shown below.

An assignment statement x := E is one of the most popular types of statement. It assigns the value of an expression E to a variable x. The WP for an assignment wp(x:=E,Q) is obtained by substituting all occurences of x in Q with the expression E.

WP(x := E, Q) = Q[x/E]

Example:

WP(x:=3, x + y = 10)
= 3 + y = 10 
= y = 7
Thus, we have {y=7} x := 3 {x + y = 10}

WP(x:=3, {x + y > 0) 
= 3 + y > 0  
= y > -3
Thus, we have {y > -3}  x := 3 {x + y> 0}


WP(x:=3, {y > 0) 
= y > 0    # because there is no `x` in `y > 0`, the result is just `y > 0`
Thus, we have {y > 0}  x := 3 y > 0}

A list of sequential statements. The WP for list is defined recursively as follows.

WP([S1; S2; S3 ...;]  Q) = WP(S1, WP(S2;S3;.., Q))
WP([], Q) = Q

Example:

WP([x:=x+1; y:=y*x], y=2*z) 
=   WP(x:=x+1, WP([y:=y*x], y=2*z))
=   WP(x:=x+1, y*x=2*z)
=   y*(x+1)=2*z
Thus, we have {y*(x+1)=2*z}  x:=x+1; y:=y*x {y=2*z}

The WP of a conditional statement if b then S1 else S2, Q combines the WPs of S1 and S2.

WP(if b then S1 else S2, Q)  =  (b => WP(S1,Q))  &  (!b => WP(S2, Q))

Example:

WP(if x > 0 then y := x + 2  else y := y + 1,  y > x) 
= (x > 0 => WP(y := x + 2, y > x) & (x<=0 => WP(y := y + 1, y > x))
= (x > 0 => x + 2 > x)  &  (x <= 0 => y + 1 > x)
= (x > 0 => 2 > 0)      &  (x <= 0 => y + 1 > x)
=     True              &  (x <= 0 => y + 1 > x)
=            x <= 0 => y + 1 > x

WP(if x > 0 then y :=x  else y:= 0,  y > 0) 
= (x>0 => WP(y:=x, y >0)) & (x<=0 => WP(y:=0, y>0))
= (x > 0 => x > 0)      &  (x <= 0  =>  0 > 0)
= !(x > 0) || (x > 0)   &  !(x <= 0) || False
=       True           &         x > 0   
=                    x > 0  

Note: Instead of using => (imply), which might be confusing to some, we can use just ! (not) and || (or)

WP(if b then S1 else S2, Q)
=  (b => WP(S1,Q))  &  (!b => WP(S2, Q))
=  !((b & !WP(S1,Q))  ||  (!b & !WP(S2, Q)))

Unlike other statements where we have rules to compute WP automatically, for loop, we (the user) need to supply a loop invariant I obtain the WP of loop. The WP for loop is:

    WP(while [I] b do S, Q) =    I   &   (I & b) => WP(S,I)    &  (I & !b)  => Q   

As can be seen, the WP for loop consists of 3 conjuncts:

1. I : the loop invariant (should hold when entering the loop)
2. (I & b) => I : (entering the loop because b is true) I is preserved after each loop body execution
3. (I & !b) => Q (exiting the loop because b is false), when exiting the loop, the post condition holds

Example:

Let's consider the while loop

while(i < N){
  i:=N
}

# note that this is equivalent to 

while(True){
  # [I]: loop invariants here
  if(!i < N) break;
  i := N;
}

Assume that we have found two loop invariants at [I] for this loop

• i <= N
• N >= 0
• True # and yes, True is always a loop invariant (though very weak and likely useless)

Let's compute the WP of this loop using these loop invariants; also let's use i == N as Q

# Using loop invariant i <= N
WP(while[i <= N] (i < N ) i := N, i == N)
=  i <= N & (i <= N & i < N) => WP(i := N, i <= N) & (i <= N & !(i < N))  => i == N)
# let's deal these 3 conjuncts one by one, easier that way

1. i <= N

2. (i <= N & i < N) => WP(i := N, i <= N)
   = i < N          =>  N <= N
   = i < N          =>   True
   =        True

3. (i <= N & !(i < N))  => i == N)
   = (i <= N  & i >= N)  => i == N
   =     i == N   =>  i == N
   =          True
   
# so these 3 conjuncts become
i <= N  & True  & True
= i <= N    #  the WP of the while loop



# Using loop invariant N >= 0
WP(while[N >= 0] (i < N ) i := N, i == N)    
=  N >= 0 & (N >= 0 & i < N) => WP(i:= N, N >= 0) & (N >= 0 & !(i < N))  => i == N)
# let's deal these 3 conjuncts one by one

1. N >= 0

2. (N >= 0 & i < N) => WP(i:= N, N >= 0)
   = (N >= 0 & i < N) =>  N >= 0
   =    True     # because a & b = > a  is True

3. (N >= 0 & !(i < N))  => i == N)
   = (N >= 0  & i >= N)  => i == N   # can't simplify much further, so just leave as is
 
   
# so these 3 conjuncts become
N >= 0 &  (N >= 0  & i >= N)  => i == N  #  the WP of the while loop

# Using loop invariant True
WP(while[True] (i < N ) i := N, i == N)    
=  True & (True & i < N) => WP(i:= N, True) & (True & !(i < N))  => i == N)

1. True

2. (True & i < N) => WP(i:= N, True)
   = True & i < N =>  True   
   =   True 

3. (True & !(i < N))  => i == N)
   = (i >= N)  => i == N   # can't simplify much further, so just leave as is
 
   
# so these 3 conjuncts become
i >= N  => i == N  #  the WP of the while loop

Thus, we get different WPs when we use different loop invariants. As we will see later, this can affect our verification task. That is, if we pick a good or strong invariant, we can prove the program. But if we pick a weak one, we might not be able to prove the program.

Now that we know how to do WP, we can continue with verifiation condition (VC). Recall that to verify that the program S satisfies the precondition P and postcondition Q (i.e., the Hoare triple {P} S {Q} is valid), we create the VC P => WP(S, Q) and check its validity, i.e., if the VC becomes True. If the VC is valid, we have proved the program (i.e., it's correct wrt to the specs); otherwise, we cannot say anything about the program, i.e., we don't know if it's correct or not.

Example:

Consider the following program (note: this while loop is the same as the example in the LOOP section).

# {N >= 0} precondition 
i := 0;
while(True){
  # [I]: loop invariants here
  if(!i < N) break;
  i := N;
}
# {i == N}  post condition

Let's prove that it is correct wrt to the given specs.

P => WP(S, Q)   # create VC
(N >= 0) => WP([i:=0, while(...)], i == N)
(N >= 0) => WP(i:=0, wp(while(...), i == N))  # wp rule for list of statements

We need to compute the WP of the loop, which has many invariants at [I], e.g., N >= 0, i>=0, i <= N, True.

1. Let's use the loop invariant i <= N and as shown here, we get the WP of the loop as i <= N. We continue contructing the VC

   (N >= 0) => WP(i := 0, wp(while[i <= N](...), i == N))  # wp rule for list of statements
   (N >= 0) => WP(i := 0, i <= N)  # wp of while becomes i <= N as shown above
   (N >= 0) => (0 <= N)  # wp for assignment
   True
   

   The VC becomes True and thus we were able to prove the program is correct wrt to the given specification.

2. Let's now use N >= 0 as the loop invariant and as shown here, we get the WP of the loop as N >= 0 & (N >= 0 & i >= N) => i == N.

   (N >= 0) => WP(i := 0, wp(while[N >= 0](...), i == N))  # wp rule for list of statements
   (N >= 0) => WP(i := 0, N >= 0 &  ((N >= 0  & i >= N)  => (i == N))  # wp of while becomes i <= N as shown above
   (N >= 0) =>  (N >= 0 &  ((N >= 0  & 0 >= N)  => (0 == N)) # wp for assignment
   (N >= 0) =>  (N >= 0 &  0 == N  => 0 == N) # 
   (N >= 0) =>  (N >= 0 &    True) 
   (N >= 0) =>  (N >= 0)
   True
   

   The VC is also True and once again have proved the program is correct wrt to the given specification.

3. What if we use True? The WP of the while loop using this loop invariant, as shown above, will be i >= N => i == N. We now use it to construct the VC:

(N >= 0) => WP(i:=0, wp(while[i<= N](...), i == N))  # wp rule for assignment
(N >= 0) => WP(i:=0, i >= N  => i == N)  # wp of while
(N >= 0) =>  (0 >= N  => 0 == N) # wp for assignment
True

The VC is also True and once again have proved the program is correct wrt to the given specification.

####################

Thus we first will compute the wp of the program wrt to the postcondition Q However, because this program contains a loop, so we need to provide a loop invariant.

2. What if we use a different loop invariant N >= 0. The WP of the while loop using this loop invariant, as shown above, will be N >= 0 & (N >= 0 & i >= N) => i == N . We now use it to construct the VC:

(N >= 0) => WP(i:=0, wp(while[i<= N](...), i == N))  # wp rule for assignment
(N >= 0) => WP(i:=0, N >= 0 &  (N >= 0  & i >= N)  => (i == N)  # wp of while as shown above
(N >= 0) => (N >= 0 & (N >= 0 & 0 >= N) => 0 == N)  # wp for assignment
(N >= 0) => (N >= 0 & True)  # wp for assignment
True

wp(i := 0; while[i<=N] i < N do i:= N], i == N)

. Also, the program can be written as , with precondition P: N >= 0and postconditionQ: i==N`.

1. Example: using a sufficiently strong invariant

   Here, we use the loop invariant i <= N to prove S is correct wrt to P,Q. As we will see, this loop invariant is sufficiently strong because it allows us to prove the program.

   1. Apply the WP to the program, which is a list of statements.

      WP([i := 0; while[i<=N] i < N do i:= N], i = N) 
      = WP(i := 0; WP(while[i<=N] i < N do i:=N], i = N)  #WP rule for list of statements
      

   2. Apply the WP to while

      # Let's first compute WP(while[i<=N] i < N do i:=N, {i = N}). According to the WP rule for LOOP, we will have 3 conjuncts 
      1. i <= N
      
      2. (i <= N & i < N) => WP(i:=N, {i<=N})
         = i < N          =>  N <= N 
         = i < N          =>  True   
         = True     # because !(i<N) or True  is true (anything or with true is true)
      
      3. (i <= N & !(i<N)) => i = N
         = i = N           => i = N
         = True     # because !(i=N) | i = n  is True (a or !a is True)
      
      =  i <= N & True & True
      =  i <= N
      

   3. After obtaining the WP i<=N for while, we continue with WP(i:=0, i<=N)

      # WP([i := 0; while[i<=N] i < N do i:= N], i = N) = WP(i := 0, i<=N)
      WP(i := 0, i<=N)
      = 0<=N  #WP rule for assignment
      

   4. Now we construct a verification condition (vc) to check that the given precondition P: N >= 0 implies the WP 0<=N

      P => WP([i := 0; while[i<=N] i < N do i:= N], {i = N}) 
      = N>=0 =>  0<=N   # N>=0 is the given precondition and 0 <= N is the WP we obtain above for the program
      = True
      

      Because te given precondition N>=0 implies 0<=N, the Hoare tripple is valid, i.e., the program is correct.

   5. Also, the loop invariant i <= N is thus sufficiently strong to let us prove the program satisfy the specifications.

2. Example 2: using an insufficiently strong invariant

   Here, we use the loop invariant N >= 0 to prove program. As we will see, this loop invariant is not sufficiently strong because we will not be able to use it to prove the program.

   1. Apply the WP to while

      WP(while[N >= 0] i < N do i:=N, {i = N})
      =
        1. N >= 0
        2. (N >=0 & i < N) => WP(i := N, N >= 0) = 
           (N >=0 & i < N) => i >= 0   # we can't simplify much, so just leave as is
      
        3. N >=0 & !(i<N) => i =N
           (N >= 0 & i >= N) => i = N
           i>= 0  => i = N  # we can't simplify much, so just leave as is
      
        =  N >=0 & (N >=0 & i < N) => i >= 0 & (i>= 0  => i = N)
      
      WP(i:=0; {N >=0 & (N >=0 & i < N) => i >= 0 & (i>= 0  => i = N)})
        = (0 >= 0) & (0 >= 0 & 0 < N => 0 >= 0) & (0>=0 => 0 = N)  #apply WP for assignment and simplify
        =  TRUE    &      TRUE                  & 0 = N
        = 0 = N
      

   2. Obtain the vc

      P => 0 = N  # the given precondition implies 0 = N
      (N >= 0) => 0 = N  # This is not valid, e.g., counterexample N=3
      

      The vc is not valid and thus we were not able to prove the Hoare triple and hence do not know whether the program is correct or not.

   3. Thus this loop invariant is not sufficiently strong for us to prove the program.

      Important: as mentioned, not being able to prove simply means we cannot prove it using this loop invariant. It does not mean that you disprove it or show that the Hoare triple is invalid. (in fact, we know the Hoare tripple is valid if we used a different loop invariant, e.g., i <= N )

At a high level, loop invariant capture the meaning of the loop, and thus help understand and reason about the loop. They are especially helpful for automatic verification (e.g., using Hoare logic).

A loop invariant is a property I that always holds at the loop entrance. This means that I (i) holds when the loop entered and (ii) is preserved after the loop body is executed. I is also called an inductive loop invariant.

If you have a loop that looks like

while (b){
  #loop body
}

It is useful to transform it to this equivalent form

while (True){
  # [I] : loop invariant I is right here
  if (!b) break
  #loop body
}

Then the loop invariant I is right when you enter the loop, as indicated by [I] in the code above.

Note that I is not located after the guard condition b is satisfied, e.g.,

while (b){
  #[I]  : incorrect location for loop invariant
  #loop body
}

We will use an example to demonstrate loop invariants. Consider a simple program

# {N >= 0}  # pre condition
i := 0;
while(i < N){
  i := N;
}
# {i = N} # post condition

To make it easier to see where loop invariants are, we first transform this program into an equivalent one:

# {N >= 0} pre condition
i := 0;
while(True){
  # [I]: loop invariants here
  if(!i < N) break;
  i := N;
}
# {i = N} post condition

The while loop in this program has many possible loop invariants (any property that is true at [I]):

1. True : is always a loop invariant, but it is very weak and trivial, i.e., almost useless for any analysis
2. N >= 0: because N>0 is a precondition and N is never changed
3. i>=0: because i is initalized to 0 can only changed to N, which itself is >=0 and never changed.
4. i <= N: because i can only either be 0 or N, and N >=0.

An important question to ask is which loop invariants are useful? Typically, the more stronger the better as they capture the meaning of the loop more precisely (thus true is not very useful). However, the answer really depends on the task we are trying to achieve. If the task is to prove a very weak (trivial) property, then we might not need strong loop invariants, e.g., for instance to prove that N >= 0 as the postcondition, then we only need the loop invariant N >= 0. Vice versa, if the task is to prove a strong property such as i=N, then we likely need strong loop invariants, e.g., i<=N.

In many cases, we can guess which loop invariants are useful based on the postconditions we want to prove. However, in the general cases we do not know a priori which loop invariants to use. If the program is indeed correct wrt the specs (i.e., the representing Hoare tripple is valid), there are two possible scenarios about using loop invariants to prove programs:

1. if we use sufficiently strong loop invariants, then we will be able to prove the program is correct.
2. if we use insufficiently strong loop invariants, then we will not* be able to prove the program is correct.

The loop section in Hoare logic gives concrete examples demonstrating these two cases.

Thus, this gives an crucial observation**: if we can prove that a program is correct (e.g., using Hoare logic), then it is really correct. However, if we cannot prove that the program is correct, then we do not know whether the program is correct or not: it could be wrong, or it is actually correct but we can't prove it.