How do I write a clean function in Dafny to get the minimum of a set?

Question

I am trying to write a function to get the minimum of a non-empty set.

Here is what I came up with:

method minimum(s: set<int>) returns (out: int)
requires |s| >= 1
ensures forall t : int :: t in s ==> out <= t
{
  var y :| y in s;
  if (|s| > 1) {
    var m := minimum(s - {y});
    out := (if y < m then y else m);
    assert forall t : int :: t in (s - {y}) ==> out <= t;
    assert out <= y;
  } else {
    assert |s| == 1;
    assert y in s;
    assert |s - {y}| == 0;
    assert s - {y} == {};
    assert s == {y};
    return y;
  }
}

This is suboptimal for two reasons:

Dafny gives a "No terms found to trigger on." warning for the line,
```
assert forall t : int :: t in (s - {y}) ==> out <= t;
```
However, removing this line causes the code to fail to verify. My understanding is that the trigger warning isn't really bad, it's just a warning that Dafny might have trouble with the line. (Even though it actually seems to help.) So it makes me feel like I'm doing something suboptimal or non-idiomatic.
This is pretty inefficient. (It constructs a new set each time, so it would be O(n^2).) But I don't see any other way to iterate through a set. Is there a faster way to do this? Are sets really intended for programming "real" non-ghost code in Dafny?

So my question (in addition to the above) is: is there a better way to write the minimum function?

score 1 · Answer 1 · answered May 08 '18 at 00:42

In this case, I recommend ignoring the trigger warning, since it seems to work fine despite the warning. (Dafny's trigger inference is a little bit overly conservative when it comes to the set theoretic operators, and Z3 is able to infer a good trigger at the low level.) If you really want to fix it, here is one way. Replace the "then" branch of your code with

var s' := (s - {y});
var m := minimum(s');
out := (if y < m then y else m);
assert forall t :: t in s ==> t == y || t in s';
assert forall t : int :: t in s' ==> out <= t;
assert out <= y;

The second problem (about efficiency) is somewhat fundamental. (See Rustan's paper "Compiling Hilbert's Epsilon Operator" where it is mentioned that compiling let-such-that statements results in quadratic performance.) I prefer to think of Dafny's set as a mathematical construct that should not be compiled. (The fact that it can be compiled is a convenience for toy programs, not for real systems, where one would expect a standard library implementation of sets based on a data structure.)

How do I write a clean function in Dafny to get the minimum of a set?

1 Answers1

Linked