# Class 17: SOP: Array Assertions

Back to SOP: Predicates. On to SOP: Gries-Style Documentation.

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:

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] = ( 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?

Back to SOP: Predicates. On to SOP: Gries-Style Documentation.

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 Wed Mar 2 11:39:18 2005.
The source to the document was last modified on Tue Jan 25 12:37:38 2005.
This document may be found at http://www.cs.grinnell.edu/~rebelsky/Courses/CS302/2005S/Outlines/outline.17.html.

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

Samuel A. Rebelsky, rebelsky@grinnell.edu