Vector.dfy

// A simple implementation of dynamically resizing arrays.

class Vector<T(==)> {
  var data: array<T>;
  var size: int;

  ghost var Repr: set<object>;
  ghost var contents: seq<T>;

  predicate Valid()
    reads this, Repr
  {
    this in Repr && null !in Repr && data in Repr &&
    0 <= size <= data.Length &&
    0 < data.Length &&  // convenient so that doubling length is strictly increases it
    contents == data[..size]
  }

  constructor ()
    modifies this
    ensures Valid()
    ensures contents == []
    ensures fresh(Repr - {this})
  {
    data := new T[10];
    size := 0;

    Repr := {this};
    Repr := Repr + {data};

    contents := [];
  }

  // Grow the Vector to the given capacity.
  method Resize(goal: int)
    requires Valid()
    requires goal > data.Length
    modifies this
    ensures Valid()
    ensures fresh(Repr - old(Repr))
    ensures contents == old(contents)
    ensures data.Length == goal
  {
    var a := new T[goal];
    var i := 0;
    while i < size
      invariant 0 <= i <= size
      modifies a
      invariant forall j :: 0 <= j < i ==> a[j] == data[j]
    {
      a[i] := data[i];
      i := i + 1;
    }

    data := a;
    Repr := (Repr - {data}) + {a};
  }

  // Add an element to the end of the Vector
  method Push(t: T)
    requires Valid()
    modifies Repr
    ensures Valid()
    ensures contents == old(contents) + [t]
    ensures fresh(Repr - old(Repr))
  {
    if size == data.Length {
      Resize(2 * data.Length);
    }

    data[size] := t;
    size := size + 1;
    contents := contents + [t];
  }

  // Remove an element from the end of the Vector
  method Pop()
    requires Valid()
    requires size > 0
    modifies Repr
    ensures Valid()
    ensures contents == old(contents[..size-1])
    ensures Repr == old(Repr)
  {
    contents := contents[..size-1];
    size := size - 1;
  }

  // There's no need for a Get(i) method, because clients may read
  // directly from the data array.

  // Modify the element at the given index.
  // While it is possible for clients to write directly to the data
  // array as well, they must remember to update the ghost variable
  // contents, else Valid() will not hold.  So it is convenient to
  // define this method.
  method Set(i: int, t: T)
    requires 0 <= i < size
    requires Valid()
    modifies Repr
    ensures Valid()
    ensures contents == old(contents[..i]) + [t] + old(contents[i+1..])
    ensures Repr == old(Repr)
  {
    data[i] := t;
    contents := contents[..i] + [t] + contents[i+1..];
  }

  // Check whether a given value is in the Vector
  // This is the only method that requires T be equality supporting.
  method Contains(t: T) returns (result: bool)
    requires Valid()
    ensures result <==> t in contents
  {
    var i := 0;
    while i < size
      invariant 0 <= i <= size
      invariant forall j :: 0 <= j < i ==> contents[j] != t
    {
      if data[i] == t { return true; }
      i := i + 1;
    }

    return false;
  }


  static method SelfTest()
  {
    var v := new Vector<int>();
    var i := 0;
    while i <= 100
      invariant fresh(v.Repr)
      invariant v.Valid()
      invariant v.size == i  // required so that we know the size after the loop for Set()
    {
      v.Push(i * i);
      i := i + 1;
    }

    v.Pop();

    v.Set(10, 7);

    var hasSeven := v.Contains(7);
    assert hasSeven;

    i := 0;
    while i < v.size
      invariant v.Valid()
    {
      var x := v.data[i];
      assert x in v.contents;
      print x, "\n";
      i := i + 1;
    }
  }
}

// Comment this out to use Vector as a library.
method Main()
{
  Vector<int>.SelfTest();
}