Reading Arrays

In class 18 and onward we start working with arrays, the mutable analog to immutable sequences. Our first examples in class will be writing loops to implement a variety of search algorithms.

Example: binary search

Before we start using arrays and loops, let’s warm up with plain old sequences and plain old recursion implementing plain old binary search.

Recursive search of a sequence

datatype Option<X> = None | Some(value: X)

function BinarySearch(s: seq<int>, key: int): (result: Option<int>)
  requires forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
  ensures match result
    case Some(idx) => 0 <= idx < |s| && s[idx] == key
    case None => key !in s
{
  BinarySearchIn(s, key, 0, |s|)
}

function BinarySearchIn(s: seq<int>, key: int, lo: nat, hi: nat): (result: Option<int>)
  // requires? ensures? decreases?
{
  if lo == hi then
    None
  else
    var mid := (lo + hi) / 2;
    if key < s[mid] then
      BinarySearchIn(s, key, lo, mid)
    else if s[mid] < key then
      BinarySearchIn(s, key, mid + 1, hi)
    else
      Some(mid)
}

Iterative search of a sequence

Here is the outline of a method to implement binary search with a loop instead of recursion:

method BinarySearch(s: seq<int>, key: int) returns (result: Option<int>)
  requires forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
  ensures match result
    case Some(idx) => 0 <= idx < |s| && s[idx] == key
    case None => key !in s
{
  var lo: nat, hi: nat := 0, |s|;
  while GUARD
    invariant INVARIANT
  {
    var mid := (lo + hi) / 2;
    // same cases as in the recursive implementation:
    // if s[mid] == key then return Some(mid)
    // -otherwise-
    // update hi or lo as appropriate, and keep looping
  }
  return None;
}

If we find key in the sequence, we will return early from the method: our proof obligation at that moment is to show that Some(mid) satisfies the postcondition, which will be straightforward.

Otherwise, when we reach return None, we will need ¬GUARD ∧ INVARIANT to imply key !in s.

Here is a diagram of the situation after we assign mid := (lo + hi) / 2:

The elements at indices 0 to lo-1 are too small, and the elements at indices hi to |s|-1 are too large. We are about to examine s[mid] and decide whether to update lo or hi (or return).

datatype Option<X> = None | Some(value: X)

method BinarySearch(s: seq<int>, key: int) returns (result: Option<int>)
  requires forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
  ensures match result
    case Some(idx) => 0 <= idx < |s| && s[idx] == key
    case None => key !in s
{
  var lo: nat, hi: nat := 0, |s|;
  while false
    invariant true // regarding lo and hi
    invariant true // regarding key      
  {
    var mid := (lo + hi) / 2;
    if key < s[mid] {
      // TODO
    } else if s[mid] < key {
      // TODO
    } else {
      return Some(mid);
    }
  }
  return None;
}

Arrays

Arrays are our first foray in 6.S057 into the world of mutable data. Here’s one way to create an array:

var a := new string[] [ "apple", "banana", "citron" ];
assert a.Length == 3;
assert a[0] == "apple";

Variable a is a reference to a length-3 array of strings. Recall from 6.101 the consequences of aliases to mutable data:

var b := a;
b[0] := "asparagus";
assert a[0] == "asparagus";
assert a == b;

Assigning b := a makes b an alias to the same array object in memory. Reassigning b[0] := ... is the same as reassigning a[0]. And a == b does not compare the contents of the referenced arrays, as it would for immutable sequences:

var c := new string[] [ "asparagus", "banana", "citron" ];
assert a != c;
assert a[..] == c[..];

… instead, it asks whether the references are equal: do they point to the same object? We can use the slicing operator [..] to obtain the sequence (or a subsequence) of values in an array. That sequence is, of course, immutable: if we store it in a variable, subsequent mutations of the array are not reflected in the sequence.

Iterative search of an array

Our search procedure with sequences works with arrays after only tiny spec changes:

method BinarySearch(a: array<int>, key: int) returns (result: Option<int>)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures match result
    case Some(idx) => 0 <= idx < a.Length && a[idx] == key 
    case None => key !in a[..] 
{
  var lo: nat, hi: nat := 0, a.Length;

  //
  //
  //
  // Complete the exercises above
  // before you look at the details
  // of this implementation...
  //
  // ... because they are identical :)
  //
  //
  //

  return None;
}

method BinarySearch(a: array<int>, key: int) returns (result: Option<int>)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures match result
    case Some(idx) => 0 <= idx < a.Length && a[idx] == key 
    case None => key !in a[..] 
{
  var lo: nat, hi: nat := 0, a.Length;
  while lo < hi
    invariant lo <= hi <= a.Length 
    invariant key !in a[..lo] && key !in a[hi..]
  {
    var m := (lo + hi) / 2;
    if key < a[m] {
      hi := m;
    } else if a[m] < key {
      lo := m + 1;
    } else {
      return Some(m);
    }
  }
  return None;
}

However, we are certainly going to have work to do once we start writing methods that mutate their mutable arguments!

method ''BinarySearch''(a: array<int>, key: int) returns (result: Option<int>)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  modifies a
  ensures match result
    case Some(idx) => 0 <= idx < a.Length && a[idx] == key
    case None => key !in a[..]
{
  if a.Length > 0 {
    a[a.Length/2] := key;
    return Some(a.Length/2);
  }
  return None;
}

datatype Option<X> = None | Some(value: X)

‘‘BinarySearch’’ indeed.

Summary

Arrays are the classic data structure to practice with the power of loops and loop invariants, and we’ll spend much of the remainder of the semester working with them. Arrays are the mutable counterpart to immutable sequences, and we often write specifications about arrays by first converting those arrays into sequences with slice notation. It is just easier to reason about mathematical objects that stay put, not being modified later by code. Working with arrays brings in the same gotchas of aliasing that we are used to from our prerequisite subjects. We usually write loop invariants for array programs using mixes of quantifiers over array indices and (where possible) array/sequence slice operations.