Iterating over sets

Feb 2, 2013 at 3:02 PM
How can I iterate over a set? I need to do so to construct a set from another set by inspecting the elements of that other set. I used the parallel stmt, but it wouldn't allow me to assign to a local variable (the set to be constructed).

My current solution is to define my own set data type and then I can use functional pattern matching. However, this solution has the drawback that I have to axiomatize my data type. I'd rather leverage the built-in set type and its axiomatization.
Feb 2, 2013 at 3:33 PM
Edited Feb 2, 2013 at 3:34 PM
Another approach is to use an undefined/axiomatic function to choose an element from a non-empty set:
function choose<T>(s : set<T>) : T
  requires s != {};
  ensures choose(s) in s;
If you wanted to iterate over a set you could use "choose" to pull elements out one by one:
function sum(s: set<int>): int
{
  if s == {}
  then 0
  else 
    var x := choose(s);
    x + sum(s - {x})
}
I'm not sure how well this style works with verification though.
Feb 2, 2013 at 3:50 PM
Thanks for your reply! That would be an alternative to my current workaround. I'll give it a try!

My current workaround introduces its own Set data type:
datatype Set<El> = Empty | Union(El, Set<El>);
The benefit of the approach is that I can access an element by pattern matching. The downside, however, is that I need to define further functions to convert between Set and set and for the set operations. And, worse, I have to axiomatize the set operations such that I get my program verified.
Coordinator
Feb 2, 2013 at 5:22 PM
Dafny now supports a let-such-that expression (ghost only), which lets you implement the "take" function above. In statements, you can use the assign-such-that statement. The program below shows multiple ways of iterating over set elements (I shall add it to the Dafny test suite).

Rustan
function Count<T>(s: set<T>): int
{
  if s == {} then 0 else
    var x :| x in s;  // let x be such that "x in s"
    1 + Count(s - {x})
}

method Copy<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := {};
  var r := s;
  while (r != {})
    invariant s == r + t;
    decreases r;
  {
    var x :| x in r;
    r, t := r - {x}, t + {x};
  }
}

method CopyFaster<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := {};
  var r := s;
  while (r != {})
    invariant s == r + t;
    decreases r;
  {
    var p :| p != {} && p <= r;  // pick a nonempty subset of r
    r, t := r - p, t + p;
  }
}

method CopyFastest<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := s;  // :)
}

iterator Iter<T>(s: set<T>) yields (x: T)
  yield ensures x in s && x !in xs[..|xs|-1];
  ensures s == set z | z in xs;
{
  var r := s;
  while (r != {})
    invariant forall z :: z in xs ==> x !in r;  // r and xs are disjoint
    invariant s == r + set z | z in xs;
  {
    var y :| y in r;
    r, x := r - {y}, y;
    yield;
    assert y == xs[|xs|-1];  // needed as a lemma to prove loop invariant
  }
}

method UseIterToCopy<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := {};
  var m := new Iter(s);
  while (true)
    invariant m.Valid() && fresh(m._new);
    invariant t == set z | z in m.xs;
    decreases s - t;
  {
    var more := m.MoveNext();
    if (!more) { break; }
    t := t + {m.x};
  }
}