Class 18: Array Assertions

Held: Tuesday, 18 February 2003

Summary: Today we consider some of the kinds of assertions one might make about arrays and the notations we might use for those assertions.

Related Pages:

• EBoard.

Due

• Gries 5.

Overview:

• What is an array? Additional perspectives.
• More notation.
• Multidimensional arrays.
• Array diagrams.
• Partitioning.

What is an Array? Revisited

• In our previous class, we saw a number of different models of 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 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.

• 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?

An Example: Partitioning

• We'll use array pictures to start to develop a procedure that partitions an array into two parts, things smaller than a given value and things larger than a given value.
• Sorry, the example will be developed on the fly.