Taking an element from a non-empty set

Nov 21, 2012 at 4:29 PM
Edited Nov 21, 2012 at 4:29 PM

Is there a way to take an element from a set you know to be non-empty? Viz. can I give this function a body? (For now I'm just using it as an axiom.)

function take<T>(s : set<T>) : T
  requires s != {};
  ensures take(s) in s;
Feb 2, 2013 at 4:14 PM
It looks like I am having the same problem (see my post today. Did you figure a solution to this problem in the meantime? Thanks, Stephanie.
Feb 2, 2013 at 4:28 PM
No, I just used my axiomatic "take" function.
Feb 2, 2013 at 6:16 PM
As of last week, there is such a way. :) Dafny now supports let-such-that expressions. So, you can implement your "take" function as follows:
function take<T>(s : set<T>) : T
  requires s != {};
  ensures take(s) in s;
  var x :| x in s; x
Note that the let-such-that expression is deterministic, which means that "take" is indeed a function. But compiling it into something deterministic could mean a great deal of run-time overhead, so the let-such-that expression is a ghost-only operation (which in this case means you can't make "take" into a "function method").

There is also an assign-such-statement (which has been there for a while). It's not a ghost statement. However, it is currently not supported by the compiler (but it should be, someday).

Dafny actually has a "choose" statement, from before the time it even had the assign-such-that statement. It currently compiles. However, please don't use it, because I want to remove it in favor of the assign-such-that statement. (If you need compiler support for assign-such-that, please let me know and I'll increase the priority of that. Or implement it yourself in the open sources.)

I'm about to reply to Stephanie's other question, where I will refer to an example program, which is relevant here too.