
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 builtin 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 nonempty 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.



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 letsuchthat expression (ghost only), which lets you implement the "take" function above. In statements, you can use the assignsuchthat 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[..xs1];
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[xs1]; // 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};
}
}

