Function and such that operator interaction

[rdivyanshu]

What change in documentation do you suggest?

These two seems to be at odd with each other

• See Section 7.3 for a description of the function specification. A Dafny function is a pure mathematical function.

• This form has one or more left-hand-sides, a :| symbol and then a boolean expression on the right. The effect is to assign values to the left-hand-sides that satisfy the RHS condition. .... . The given boolean expression need not constrain the LHS values uniquely: the choice of satisfying values is non-deterministic.

ghost function Any<E(!new)>(data: set<E>): E
  requires |data| != 0
{
    var key :| key in data; key
}

ghost function PredicateAny<E(!new)>(data: set<E>): bool
  requires |data| != 0
{
    var k1 :| k1 in data;
    var k2 :| k2 in data;
    k1 == k2
}

ghost function PredicateAny2<E(!new)>(data: set<E>): bool
  requires |data| != 0
{
    var k1 := Any(data); var k2 := Any(data); k1 == k2
}
  
lemma Test(s: set<int>)
  requires |s| != 0
{
    var r1 := PredicateAny(s);
    var r2 := PredicateAny2(s);
    assert r1;
    assert r2;
}

In code above assert r2 verifies but assert r1 doesn't. It seems that function referential transparency (being pure) is not followed for :| operator. Functions somehow remembers which choice it took.