CODEWITHSUNDEEP
triggersz3theorem-provingdafnymultiset
Theo Deep
Theo Deep

Reputation: 786

Trigger Dafny with multisets

This lemma verifies, but it raises the warning Not triggers found:

lemma multisetPreservesGreater (a:seq<int>, b:seq<int>, c:int, f:int, x:int)
       requires |a|==|b| && 0 <= c <= f + 1 <= |b| 
       requires (forall j :: c <= j <= f ==> a[j] >= x)
       requires multiset(a[c..f+1]) == multiset(b[c..f+1])
       ensures (forall j :: c <= j <= f ==> b[j] >= x)
{

       assert (forall j :: j in multiset(a[c..f+1]) ==> j in multiset(b[c..f+1]));

}

I do not know how to instantiate this trigger (cannot instantiate it as a function, or can I?). Any help?

Edit: Maybe I can instantiate a method f such that takes an array and inserts it in a multiset, and therefore I can trigger f(a), but that does not mention i. I will try.

Upvotes: 1

Views: 101

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Here's one way to transform the program so that there are no trigger warnings.

function SeqRangeToMultiSet(a: seq<int>, c: int, f: int): multiset<int>
  requires 0 <= c <= f + 1 <= |a|
{
  multiset(a[c..f+1])
}

lemma multisetPreservesGreater (a:seq<int>, b:seq<int>, c:int, f:int, x:int)
       requires |a|==|b| && 0 <= c <= f + 1 <= |b| 
       requires (forall j :: c <= j <= f ==> a[j] >= x)
       requires multiset(a[c..f+1]) == multiset(b[c..f+1])
       ensures (forall j :: c <= j <= f ==> b[j] >= x)
{
       assert forall j :: j in SeqRangeToMultiSet(a, c, f) ==> j in SeqRangeToMultiSet(b, c, f);
       forall j | c <= j <= f
        ensures b[j] >= x
       {
        assert b[j] in SeqRangeToMultiSet(b, c, f);
       }
}

The point is that we introduce the function SeqRangeToMultiSet to stand for a subexpression that is not a valid trigger (because it contains arithmetic). Then SeqRangeToMultiSet itself can be the trigger.

The downside of this approach is that it decreases automation. You can see that we had to add a forall statement to prove the postcondition. The reason is that we need to mention the trigger, which does not appear in the post condition.

Upvotes: 1

Related Questions