Class 18: Array Assertions

Back to Array Basics. On to Pointer Basics.

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:

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] = ( v1, ..., vn )
• 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; [i1][i2] ... [in]: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.

History

Tuesday, 7 January 2003 [Samuel A. Rebelsky]

• Created generic version to set up course.

Tuesday, 18 February 2003 [Samuel A. Rebelsky]

• Filled in the details.

Back to Array Basics. On to Pointer Basics.

Disclaimer: I usually create these pages on the fly, which means that I rarely proofread them and they may contain bad grammar and incorrect details. It also means that I tend to update them regularly (see the history for more details). Feel free to contact me with any suggestions for changes.

This document was generated by Siteweaver on Fri May 2 14:20:29 2003.
The source to the document was last modified on Tue Feb 18 14:01:31 2003.
This document may be found at http://www.cs.grinnell.edu/~rebelsky/Courses/CS195/2003S/Outlines/outline.18.html.

You may wish to validate this document's HTML ; ; Check with Bobby

Samuel A. Rebelsky, rebelsky@grinnell.edu