Loop tracing solution

• A is an array of 3 integers

Sample Loop

-- P: ∃A[0],  ∃A[1], ∃A[2] int A[] = {5, 6, 7}; int i = 0; ∀k 0 ≤ k < i, A[k] = 2*A[k] while( i < 3 ) {           A[i]=2*A[i];           i = i + 1; }

Statement i A[0] A[1] A[2] int A[] = {5, 6, 7}; int i = 0; 0 5 6 7 A[i]=2*A[i]; i = i + 1; 1 10 6 7 A[i]=2*A[i]; i = i + 1; 2 10 12 7 A[i]=2*A[i]; i = i + 1; 3 10 12 14

• Loop tracing requires determining the state of each variable.
  
• Notice:

  • while(i < 3 )
    • Initialization of the while, i = 0
    • Maintenance of the while, i = 1, 2, 3
    • Termination of the while, i = 3

  ∀k 0 ≤ k < i, A[k] = 2*A[k]

  A[k] never changes, is invariant:
  

  1. initialization: when i=0, ∀k 0 ≤ k < i, A[k] is empty so vacuously A[k]=2*A[k]
     
     
  2. maintenance: when i=1,2, and 3, ∀k 0 ≤ k < i, A[k]=2*A[k]
     
     
  3. termination: when i=3, ∀k 0 ≤ k < i, A[k]=2*A[k]
     
     

  i is one more each loop iteration implying i ≥ 3 at some point and the while will eventually terminate.

• This is a large part of correctness proofs using loop invariants.

Question 2.7.0

1. What is the postcondition?
2. If the loop invariant holds, ∀k 0 ≤ k < i, A[k] = 2*A[k], does the post condition hold?