Data Abstraction I

In classes 13 through 15 we discuss perhaps one of the most central ideas in software construction: data abstraction.

In this reading we present an informal framing of two key ideas — abstraction functions and representation invariants — that we nevertheless suspect is more rigorous than the thinking often applied by software engineers in practice. Understanding this framework will prepare you to design, document, and maintain more effective abstraction barriers between modules in your software, regardless of whether formal verification is involved.

In class we will formalize those two key ideas as tools we can use to (1) prove the correctness of modules we create and (2) allow authors of other modules that build on top of ours to prove their correctness as well. We will also look at an example in reading 15.

Abstract types

Reading 1/2 discussed static types and defined a type as a set of values along with operations on those values. In 6.101, you saw the benefits of working with abstract types: an abstract type is defined by its operations, not by its data representation. Let’s recall two Python examples:

Built-in data type dict. Before you first used a Python dictionary, you surely read through the implementation code in dictobject.c to understand how it would work? Or if not, maybe just the header file that outlines how the data in a dict are stored in memory? No? Of course not. You looked at examples to learn about the operations that manipulate dict values, and you read the Python documentation for dict which provides the specifications for all those operations. The dict type is defined for us by those operation specifications. Not by how those operations are implemented, nor by the clever data structures they use.

Custom data type Vector2D. Here are two implementations of a small Python class to represent two-dimensional vectors:

class Vector2D:
  def __init__(self, x, y):
    """ Make a new vector from the origin to (x, y). """
    self._x = x
    self._y = y

  def x(self):
    """ The x-coordinate of this vector. """
    return self._x

  def y(self):
    """ The y-coordinate of this vector. """
    return self._y

  def __abs__(self):
    """ The magnitude of this vector. """
    return (self._x**2 + self._y**2) ** .5

  def theta(self):
    """ The polar angle of this vector. """
    return degrees(atan2(self._y, self._x))

class Vector2D:
  def __init__(self, x, y):
    """ Make a new vector from the origin to (x, y). """
    self._r = (x**2 + y**2) ** .5
    self._theta = atan2(y, x)

  def x(self):
    """ The x-coordinate of this vector. """
    return self._r * cos(self._theta)

  def y(self):
    """ The y-coordinate of this vector. """
    return self._r * sin(self._theta)

  def __abs__(self):
    """ The magnitude of this vector. """
    return self._r

  def theta(self):
    """ The polar angle of this vector. """
    return degrees(self._theta)

For other parts of the program that rely on Vector2D, these two implementations provide the same operations with the same specifications*. Programmers and code that use Vector2D need not be cognizant of its implementation, they only need to understand its specification. There are several valuable ideas at work here, which we can give names to:

• Abstraction: omitting or hiding low-level details with a simpler, higher-level idea.

• Modularity: dividing a system into pieces, each of which can be designed, implemented, reasoned about, updated, and reused separately from the rest of the system.

• Encapsulation: creating a barrier around a module so that it is responsible for its own internals, and other modules cannot interfere with its integrity.

• Information hiding: hiding the details of a module’s implementation from the rest of the system, so that those details can be changed without changing other modules.

• Separation of concerns: making a particular aspect of the system’s behavior (a “concern”) the responsibility of a single module in the implementation, rather than spreading it across modules.

We have already written Dafny methods that demonstrate a number of these ideas: a method specification provides an abstraction that hides the implementation details, it is a module we can reason about independently, and local variables in the method are encapsulated. We have freedom to revise the method’s implementation because the specification provides information hiding.

Starting in class 13, we begin writing Dafny modules with similar goals, and those modules can provide abstract types.

Contrast this idea of abstract data types to that of the inductive data types we have been using so far. When we define immutable lists as a datatype…

datatype List<ET> = Nil | Cons(head: ET, tail: List<ET>)

… we fully expect that users of List will know its representation, manipulating Nil and Cons directly.

Representation invariants

Let’s implement a type that is not built into Dafny: an immutable ordered set, i.e., a sequence of unique elements. There are many possible implementations, but let’s choose a very simple one: we store the elements in a seq.

type UniqSeq<T(==)> = seq<T> // we are *not* yet hiding the implementation

function Empty<T>(): UniqSeq<T> { // function to make an empty UniqSeq
  []
}
function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> { // add an element, if new
  if elt in us then us else us + [ elt ]
}
function Size<T>(us: UniqSeq<T>): nat {                // get the size
  |us|
}
function In<T>(us: UniqSeq<T>, elt: T): bool {         // check membership
  elt in us
}
function At<T>(us: UniqSeq<T>, i: nat): T              // indexed element access
  requires i < Size(us)
{
  us[i]
}

There are some useful facts we can prove about the operations of UniqSeq:

type UniqSeq<T(==)> = seq<T> // we are *not* yet hiding the implementation

function Empty<T>(): UniqSeq<T> { // function to make an empty UniqSeq
  []
}
function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> { // add an element, if new
  if elt in us then us else us + [ elt ]
}
function Size<T>(us: UniqSeq<T>): nat {                // get the size
  |us|
}
function In<T>(us: UniqSeq<T>, elt: T): bool {         // check membership
  elt in us
}
function At<T>(us: UniqSeq<T>, i: nat): T              // indexed element access
  requires i < Size(us)
{
  us[i]
}

lemma EmptySizeZero<T>()
  ensures Size(Empty<T>()) == 0
{}

lemma EmptyInNever<T>(elt: T)
  ensures ! In(Empty(), elt)
{}

lemma WithSizeSameOrPlusOne<T>(us: UniqSeq, elt: T)
  ensures Size(With(us, elt)) == Size(us) + if In(us, elt) then 0 else 1
{}

But there are also important facts we cannot prove — because they are not true. For example:

type UniqSeq<T(==)> = seq<T> // we are *not* yet hiding the implementation

function Empty<T>(): UniqSeq<T> { // function to make an empty UniqSeq
  []
}
function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> { // add an element, if new
  if elt in us then us else us + [ elt ]
}
function Size<T>(us: UniqSeq<T>): nat {                // get the size
  |us|
}
function In<T>(us: UniqSeq<T>, elt: T): bool {         // check membership
  elt in us
}
function At<T>(us: UniqSeq<T>, i: nat): T              // indexed element access
  requires i < Size(us)
{
  us[i]
}

lemma AtHereNotAtThere(us: UniqSeq, i: nat, j: nat)
  requires i < j < Size(us)
  ensures At(us, i) != At(us, j)
{
  // this is not true as stated
}

It is clear what the author of UniqSeq intended if we examine the code in With(..). A new (?) element is only added to the seq if it is not already included, because we intend for the seq to store only unique elements. That way, the length of the sequence |us| is the correct size of the ordered set, and the element at index i in the sequence is the i^th unique element of the ordered set.

We need to distinguish carefully at this point between two sets of values:

• the abstract space of all possible values that the client of the abstract type sees and manipulates (in this example, ordered sets)
• the representation space of all possible underlying concrete values used to implement those abstract values (in this example, arbitrary sequences).

It is clarifying to examine an alternative implementation of UniqSeq:

type UniqSeq<T(==)> = seq<T> // we are *not* yet hiding the implementation

function Empty<T>(): UniqSeq<T> { // function to make an empty UniqSeq
  []
}
function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> { // add an element, if new
  us + [ elt ] // wait, what?
}
function Size<T>(us: UniqSeq<T>): nat {                // get the size
  SizeSkip(us, {})
}
function In<T>(us: UniqSeq<T>, elt: T): bool {         // check membership
  elt in us
}
function At<T>(us: UniqSeq<T>, i: nat): T              // indexed element access
  requires i < Size(us)
{
  AtSkip(us, i, {})
}

function SizeSkip<T>(s: seq<T>, skip: set<T>): nat {
  if |s| == 0 then
    0
  else if s[0] in skip then
    SizeSkip(s[1..], skip)
  else
    1 + SizeSkip(s[1..], skip + {s[0]})
}

function AtSkip<T>(s: seq<T>, i: nat, skip: set<T>): T
  requires i < SizeSkip(s, skip)
{
  if s[0] in skip then
    AtSkip(s[1..], i, skip)
  else if i == 0 then
    s[0]
  else
    AtSkip(s[1..], i - 1, skip + {s[0]})
}

With this implementation, we can prove the relationship between indexed values that eluded us above:

type UniqSeq<T(==)> = seq<T> // we are *not* yet hiding the implementation

function Empty<T>(): UniqSeq<T> { // function to make an empty UniqSeq
  []
}
function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> { // add an element, if new
  us + [ elt ] // wait, what?
}
function Size<T>(us: UniqSeq<T>): nat {                // get the size
  SizeSkip(us, {})
}
function In<T>(us: UniqSeq<T>, elt: T): bool {         // check membership
  elt in us
}
function At<T>(us: UniqSeq<T>, i: nat): T              // indexed element access
  requires i < Size(us)
{
  AtSkip(us, i, {})
}

function SizeSkip<T>(s: seq<T>, skip: set<T>): nat {
  if |s| == 0 then
    0
  else if s[0] in skip then
    SizeSkip(s[1..], skip)
  else
    1 + SizeSkip(s[1..], skip + {s[0]})
}

function AtSkip<T>(s: seq<T>, i: nat, skip: set<T>): T
  requires i < SizeSkip(s, skip)
{
  if s[0] in skip then
    AtSkip(s[1..], i, skip)
  else if i == 0 then
    s[0]
  else
    AtSkip(s[1..], i - 1, skip + {s[0]})
}

lemma AtHereNotAtThere<T>(us: UniqSeq<T>, i: nat, j: nat, skip: set<T>)
  requires i < j < Size(us)
  ensures At(us, i) != At(us, j)
{
  AtSkipHereNotAtSkipThere(us, i, j, {});
}

lemma AtSkipHereNotAtSkipThere<T>(s: seq<T>, i: nat, j: nat, skip: set<T>)
  requires i < j < SizeSkip(s, skip)
  ensures AtSkip(s, i, skip) != AtSkip(s, j, skip)
{
  if i == 0 && s[0] !in skip { AtSkipSkips(s[1..], j - 1, skip + {s[0]}); }
}

lemma AtSkipSkips<T>(s: seq<T>, i: nat, skip: set<T>)
  requires i < SizeSkip(s, skip)
  ensures AtSkip(s, i, skip) !in skip
{}

And this brings us to the idea of a representation invariant: a predicate on the representation values that must be true in order for the implementation to function correctly, and which therefore is established and maintained by all the operations of the abstract type.

• Often the most fundamental parts of the representation invariant are captured by the static type of the rep*. Here in both UniqSeq implementations the rep is a single seq, and we are guaranteed that only elements of type T will appear in it.

• But in more complex abstract types the rep will be correspondingly more complex, with relationships between data that are not captured by the types.

  UniqSeq version 2 has no such additional invariant, and notice how it pays for it in implementation code complexity: the code must handle all those weird reps. But it does! And it correctly implements the abstract type of ordered sets.

  UniqSeq version 1 has the rep invariant that elements of the seq are uniqe. Operations that make new UniqSeq values must be careful to maintain this invariant, e.g.:

  dfy

  function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> {
    if elt in us then us else us + [ elt ]
  }

  … so that other operations can rely on it, e.g.:

  dfy

  function Size<T>(us: UniqSeq<T>): nat {
    |us| // the length of the sequence *is* the size of the ordered set
  }

Whenever you build a data abstraction, make sure you articulate the representation invariant as a predicate on the concrete rep values. Often this is very straightforward, as we saw in UniqSeq version 1: “my type ensures that it represents an ordered set where elements are unique… by only storing unique elements internally.” But do not be sloppy and assume a direct relationship between invariant properties of the abstract type and invariants your implementation relies on.

Abstraction functions

For rep space R and abstract space A, the rep invariant RI(R): bool is a predicate on the rep space R that restricts it to only valid rep values that will be produced by our implementation and for which our implementation will be correct.

The abstraction function AF(R): A is a function from the rep space to the abstract space that maps every valid rep value to the abstract value it represents. Here is a depiction of the rep invariants and abstraction functions for UniqSeq:

UniqSeq v1

UniqSeq v2

Whenever you build a data abstraction, make sure you articulate the abstraction function as a function from rep values to abstract values. Do not be sloppy and think only in terms of how imagined abstract values will be stored concretely as data — that’s a concretization function I guess? — which is a recipe for writing implementation code that makes different assumptions about the rep in different cases for different operations.

Every piece of code in the implementation must accord with the abstraction function. Let’s see how that works with a few exercises:

Now, here are several different RI & AF options for CharSet. All of them use a single string for the rep. So that we can work in Dafny, assume we define:

type CharSet = string // string is a synonym for seq<char>

1. RI(s) = s[0] < s[1] < ... < s[|s|-1]
AF(s) = { s[i] | 0 <= i < |s| }

2. RI(s) = true
AF(s) = union of { c | s[2i] <= c <= s[2i+1] } for all 0 <= i < |s|/2

3. RI(s) = s contains no duplicates
   AF(s) = { s[i] | 0 <= i < |s| }

4. RI(s) = true
AF(s) = { s[i] | 0 <= i < |s| }

function Add(s: CharSet, c: char): CharSet {  s + [c]  }

function Remove(s: CharSet, c: char): CharSet {
  if |s| == 0 then s
  else if s[0] == c then s[1..]
  else [s[0]] + Remove(s[1..], c)
}

Dafny modules

In preparation for moving from informal abstraction functions and representation invariants — which you can start using in any situation where you are creating data abstractions! — to their role in verification, we need to introduce Dafny’s syntax for information hiding with modules. Here is how we can package up UniqSeq in a module with an export declaration:

module UniqSeq {

  export
    provides UniqSeq
    provides Empty, With, Size, In, At
    provides EmptySizeZero, EmptyInNever, WithSizeSameOrPlusOne

  type UniqSeq<T(==)> = seq<T>

  // functions Empty, With, etc. ...

  // lemmas EmptySizeSero, EmptyInNever, etc. ...
}

The provides keyword allows clients to see the declaration of exported items:

• the existence of generic type UniqSeq
• the signatures and pre/postconditions of the functions
• the statements of the lemmas

… without revealing their implementations:

• they cannot see that UniqSeq is implemented with seq
• nor the bodies of the functions
• nor the proofs of the lemmas

Proving without an abstraction function

module UniqSeq {

  export
    provides UniqSeq
    provides Empty, With, Size, In, At
    provides EmptySizeZero, EmptyInNever, WithSizeSameOrPlusOne

  type UniqSeq<T(==)> = seq<T>

  function Empty<T>(): UniqSeq<T> {
    []
  }
  function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> {
    if elt in us then us else us + [ elt ]
  }
  function Size<T>(us: UniqSeq<T>): nat {
    |us|
  }
  function In<T>(us: UniqSeq<T>, elt: T): bool {
    elt in us
  }
  function At<T>(us: UniqSeq<T>, i: nat): T
    requires i < Size(us)
  {
    us[i]
  }

  lemma EmptySizeZero<T>()
    ensures Size(Empty<T>()) == 0
  {}

  lemma EmptyInNever<T>(elt: T)
    ensures ! In(Empty(), elt)
  {}

  lemma WithSizeSameOrPlusOne<T>(us: UniqSeq, elt: T)
    ensures Size(With(us, elt)) == Size(us) + if In(us, elt) then 0 else 1
  {}
}

module Client {
  import UniqSeq // we cannot see the implementations!

  method Example() {
    var empty := UniqSeq.Empty<int>();
    var one := UniqSeq.With(empty, 1);
    // we cannot examine e.g. |empty| any more, but:
    UniqSeq.EmptySizeZero<int>();    // this lemma       
    assert UniqSeq.Size(empty) == 0; // gets us this fact
    
    assert ! UniqSeq.In(empty, 1);
    
    assert UniqSeq.Size(one) == 1;
  }
}

Invoking these lemmas is quite tedious, and we will discuss how to improve that aspect of the situation in the future. But we can also see how the client’s reasoning is absolutely limited to the lemmas we provided. We provided no lemmas about At, so the client’s ability to reason about At is more or less nonexistent.

For an expressive, easily used specification of At, it would be convenient to be able to talk about the abstract value: At(us, i) is the i^th element of the abstract ordered set. Adding an abstraction function to the module interface is how we will achieve that.

Proving without a representation invariant

type UniqSeq<T(==)> = seq<T> 

function Empty<T>(): UniqSeq<T> {
  []
}
function With<T>(us: UniqSeq<T>, elt: T): UniqSeq<T> {
  if elt in us then us else us + [ elt ]
}
function Size<T>(us: UniqSeq<T>): nat {  |us|  }
function In<T>(us: UniqSeq<T>, elt: T): bool {  elt in us  }
function At<T>(us: UniqSeq<T>, i: nat): T
  requires i < Size(us)  {  us[i]  }

lemma EmptyAndWithValid<T>(us: UniqSeq<T>, elt: T)
  ensures Valid(Empty<T>())
  ensures Valid(us) ==> Valid(With(us, elt))
{}

lemma AtHereNotAtThere(us: UniqSeq, i: nat, j: nat)
  requires Valid(us)
  requires i < j < Size(us)
  ensures At(us, i) != At(us, j)
{}

ghost predicate Valid(us: UniqSeq) {
  ???
}

lemma Example() {
  var empty := Empty<int>();
  var oneTwoThree := With(With(With(empty, 1), 2), 3);
  assert Valid(oneTwoThree);
  AtHereNotAtThere(oneTwoThree, 0, 2);
}

A Valid predicate like this one is the standard form we will give our representation invariants.

Summary

One of the keys to building and maintaining large software projects is dividing them up into manageable pieces, which may be the responsibilities of separate teams. In a sufficiently complex project, it simply isn’t feasible for every engineer to understand the details of all the pieces. Data abstraction is a key technique to manage understandable promises associated with pieces of code, commonly called modules (not just in Dafny), libraries, and so on. The idea is that a code module pretends to be a simpler one. An abstraction function explains how the make-believe works, translating the real (concrete) representation into the imaginary (abstract) one. A representation invariant explains which real representations are legal to go through that transformation. While other classes in software engineering ask students to apply those ideas informally, we’re lucky to have Dafny to check that they are applied correctly.