Class 17: SOP: Array Assertions

Held: Wednesday, March 2, 2005

Summary: Today we consider ways to represent and reason about assertions one might make regarding arrays and the values stored in them.

Related Pages:

• EBoard.
• Questions and Answers on Gries, Chapter 5.

Overview:

• What is an array?
• Whee! Notation.
• Example.

What is an Array? Revisited

• From our experience in CS, we know of a variety of ways to think about arrays.
• From the implementation perspective, an array is often a contiguous area of memory.
• From the user perspective, an array is a data structure that supports a few key operations:
  • Create an array of a particular size, containing a particular type.
  • Get the value at position i in the array.
  • Set the value at position i in the array.
  • Get the number of elements in the array.
  • Get the lower bound of the array.
  • Get the upper bound of the array.
• While many data structures might support similar operations, arrays have the added benefit that get and set are usually constant-time operations.
• Gries introduces at least two other perspectives.
  • An array is a convenient way of looking at a set of subscripted variables.
  • An array is a convenient way of looking at a mutable partial function.

Some Notation

• How do we declare an array of a particular size?
  • b[lb:ub] = ( v₁, ..., v_n )
  • Note that this is an assertion about the contents of an array.
• How do we get a particular value in an array?
  • b[i]
  • b can be any expression denoting an array.
  • i can be any expression denoting an index.
  • We will use these types of values as parts of assertions.
• How do we set a particular value in an array?
  • We create a new array whose name is (b; i:v)
  • That represents an array just like b, except that the ith value is v.
  • Note that b[i] = v has a different effect: It asserts information about the current value.
• What other kinds of operations can we apply?
  • Subscripting: Extract a range of elements from an array.
    b[lb:ub]
  • Bounding: Get the lower or upper bound (no particular notation)
  • Getting the domain.
• What other kinds of assertions can we apply?
  • Arrays a and b are permutations of each other
    perm(a, b)
  • Array a is in sorted order
    ordered(a)
• Many assertions are context sensitive Consider b[1:5] = x.
• if x is an integer, asserts that b[1] = x and ... b[5] = x.
• alternately, for all i from 1 to 5, inclusive, b[i] = x.
• if x is an array, asserts that the corresponding values are the same.

Multidimensional Arrays

• As you might quess, Gries's notation supports multidimensional arrays (which you can think of as arrays of arrays (of arrays of ...).
• Gries is much stricter about typing than C. An array of arrays of integers is not the same as an array of integers.
  • In fact, there's no explicit information on implementation.
• Somewhat weird notation for making variants:
  (b; [i₁][i₂] ... [i_n]:v)
• Even more interesting interpretation:
  • (b; :g)[j] = g
  • (b; [i]I:g):[i] = (b[i]; I:g)
  • (b; [i]I:g):[j] = b[j] (where i != j)

Array Pictures

• Sometimes a picture is worth a thousand assertions (or at least a few).
• Draw a rectangle for the array.
• Put in vertical bars at points of interest.
• Place the indices near those bars.
• Put assertions about portions of the array within those portions.
• For example,

   0               s                    l           n-1
  +-----------------+------------------+---------------+
  |   <= x          |                  |    > x        |
  +-----------------+------------------+---------------+
  

• Some of these visual assertions can be misleading.
  • Consider the picture above.
  • What does it suggest about the number of values in 0..S?
  • What if s is 0?