SE 504 Formal Methods and Models
Spring 2026
HW #7: Programs Involving Assignments to Arrays
Due: 8:00pm, Wednesday, April 29

1. Calculate (and simplify as much as possible).
(a) wp.(b[i] := k).(b[i] ≠ b[k])
(b) wp.(b[b[k]] := b[j]).(b[k] = b[j])

As you will recall, the assignment command b[i] := E is really a shorthand for b := b(i:E), which can be interpreted to say

Assigned to b is the array identical to itself, except that the value of E occupies location i.

Also recall these laws:

Array Element
Evaluation Law		 b(i:E)[j]  =  if(i=j, E, b[j])
Weakest Precondition
Array Element
Assignment Law		 wp.(b[i] := E).Q  ≡  Q[b := b(i:E)] ∧ 0≤i<b.Length

Finally, you should find useful the axioms and theorems of the family of if functions.

2. Complete the development of the program below (written in Dafny but with a few liberties taken) and show a proof of (ii) from the loop checklist. (That is, prove that execution of the loop body preserves the truth of the loop invariant. The four other items on the loop checklist are clearly true.) Of course, E refers to an unknown expression. You will need to augment the loop invariant with a third conjunct in a way similar to what was done in solving the Prefix Sums problem. Note that B is a ghost variable (representing the original contents of b) and therefore cannot be mentioned in any executable command. You can assume that min is an infix binary operator that can be used in executable statements (like it is used within the postcondition). 

method Prob2(b: array<int>, ghost B: array<int>)
   requires b == B  // meaning B refers to the original contents of b
   // N is being used as an abbreviation for b.Length
   ensures Q: (∀i | 0≤i<N : b[i] = B[i] min B[i+1]) ∧ b[N] = B[N]
{
   var k: nat := 0;
   while k ≠ N
      decreases N - k
      invariant I: (∀i | 0≤i<k : b[i] = B[i] min B[i+1]) ∧ 0≤k≤N
   { 
      k,b := k+1,b(k:E);
   }
}

3. Complete the development of the program below (again, in Dafny with some liberties taken) and show a proof of (ii) from the loop checklist. (The four other items on the list are clearly true, with the exception of item (i) with respect to any fresh variables that you might introduce.) Of course, E refers to an unknown expression. You will need not only to augment the loop invariant as in the previous problem but also to strengthen it by introducing a fresh variable. You should find that using a multiple assignment command is very convenient. Don't forget that B is a ghost variable and therefore cannot be mentioned in any executable command. 

method Prob3(b: array<int>, ghost B: array<int>)
   requires b == B  // meaning B refers to original contents of b
   requires b.Length != 0
   ensures Q: (∀i | 1≤i<N : b[i] = B[i] - B[i-1]) ∧ b[0] = B[0] 
   // N is being used as an abbreviation for b.Length
   var k: nat := 1;
   while k ≠ N 
      decreases N - k
      invariant I: (∀i | 1≤i<k : b[i] = B[i] - B[i-1]) ∧ 1≤k≤N
   {
      k,b := k+1,b(k:E);
   }
}

4. Prove the correctness of the following program (written in Dafny, with a few liberties taken), which sorts an array. (Do you recognize the underlying sorting algorithm?) Because it is obvious that items (i), (iii), (iv), and (v) on the loop checklist are satisfied, all you need to show is item (ii). (And regarding (ii), all you need to consider is the line of code that swaps two array elements, as is explained below.) 

method sort(b: array<int>, ghost B: array<int>)
   requires b == B  // meaning B refers to original contents of b
   // N is being used as an abbreviation for b.Length
   ensures Ascending(b,0,N)
   ensures multiset(b[..]) == multiset(B[..])

   var m: nat := N
   while m ≠ 0 
      decreases m
      invariant I1: Ascending(b,m,N) 
      invariant I2: Boundary(b,m) 
      invariant I3: 0≤m≤N 
      invariant I4: multiset(b[..]) == multiset(B[..])
      // I: I1 ∧ I2 ∧ I3 ∧ I4
   {
      {{I ∧ m≠0}}
      var k: nat := locOfMax(b,0,m);
      {{I ∧ 0≤k<m ∧ b[k] = (MAX i | 0≤i<m : b[i]) }}
      swap(b,k,m-1);
      {{I(m:=m-1)}}
      m := m-1;
      {{I}}
   } 
}
 where
Ascending(b,p,q) : (∀i,j | p≤i≤j<q : b[i] ≤ b[j])
Boundary(b,p) : (∀i,j | 0≤i<p ∧ p≤j<N : b[i] ≤ b[j])
multiset(b[..]) == multiset(B[..]) : arrays b[] and B[], viewed as multisets, are equal

Notes/Hints:

  1. The expression b[k] = (MAX i | 0≤i<m : b[i]), which appears as a conjunct in one of the intermediate assertions (see below) within the loop body, can be replaced by the expression (∀j | 0≤j<m : b[k] ≥ b[j]). That's because they are equivalent in any context in which 0≤k<m (which is a companion conjunct) also holds. That is,

    0≤k<m  ⟹  (b[k] = (MAX i | 0≤i<m : b[i]) ≡ (∀j | 0≤j<m : b[k] ≥ b[j]))

    So use whichever of those two expressions is more amenable to completing the proof.

  2. The loop body is annotated with "intermediate assertions"; all that you must show in order to prove (ii) on the loop checklist is the Hoare Triple involving the command that calls the swap() subprogram, the precondition of which reflects the fact that the value returned by the call locOfMax(b,0,m) is a location containing the maximum value within b[0..m).

    The command swap(a,i,j) is, in effect, the assignment a := a(i,j : a[j],a[i]) and therefore (in accord with the wp array element assignment law) has the following semantics:

    wp.(swap(a,i,j).Q = Q(a := a(i,j : a[j],a[i]))

    where (provided that i=j implies E = F)

    a(i,j : E,F)[r]  = { E if i=r
    F if j=r
    a[r] otherwise

    Using the if function, this can be written as follows:

    a(i,j : E,F)[r]  =  if(i=r, E, if(j=r, F, a[r]))

  3. In carrying out the proof, you will need to refer to the array b(k,m-1 : b[m-1],b[k]) several times. Rather than writing out that entire expression each time, give it a shorter name, such as b', state its relevant properties, and then use those properties when appropriate. Which properties? Well, b'[k] = b[m-1], b'[m-1] = b[k], and, for all j equal to neither k nor m-1, b'[j] = b[j].

    Thus, if b'[i] occurs within a quantification in which i is a dummy that varies over a range that includes neither k nor m-1, you can cite the Irrelevant Array Element Axiom to justify replacing that occurrence of b'[i] by b[i].

  4. By virtue of the fact that every change made to array b[] is to swap two of its elements, the condition multiset(b[..]) == multiset(B[..]) is clearly an invariant of the program. Hence, do not bother to prove it. Nor will assuming it aid in proving any other conjunct of the loop invariant. Hence, you can just ignore it altogether.

To summarize, what you are being asked to do is to prove this Hoare Triple:

{{ I1,2,3 ∧ 0≤k<m ∧ b[k] = (MAX i | 0≤i<m : b[i]) }}
swap(b,k,m-1);
{{ (I1,2,3)[m:=m-1] }}

where I1,2,3 is shorthand for I1 ∧ I2 ∧ I3.