CODEWITHSUNDEEP
dafny
Gaurang Tandon
Gaurang Tandon

Reputation: 6753

Dafny: no terms found to trigger on and a consequent assertion error

This is the code that I wrote for a method that returns the maximum of two integers:

predicate greater(x: int, a: int, b: int){
    (x >= a) && (x >= b)
}

method Max(a: int, b: int) returns (max: int)
    ensures max >= a
    ensures max >= b
    ensures forall x /*{:trigger greater(x,a,b)}*/ :: (greater(x,a,b)) ==> x >= max
{
    if (a > b){
        max := a;
    }else{
        max := b;
    }
//  assert greater(max, a, b); - trivial assertion
}

method Main(){
    var res:= Max(4, 5);

    assert res == 5;
}

As you can see, I have tried both the two techniques metnioned in the Wiki page (manual trigger assignment and also adding a trivial non-useful assertion in the method body. However, I still get an assertion error.

I am not sure what else to do. I have read other answers like this, this and this, but none have helped me so far.

PS: I know there is a simpler way to write the postconditions for this particular method, however, I really wish to model the postconditions in terms of the forall quantifier only.

Upvotes: 3

Views: 157

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

Let's forget greater for a while and just take a look at what you're trying to achieve. After the call to Max in Main, you know the following (from the postcondition of Max):

res >= 4
res >= 5
forall x :: x >= 4 && x >= 5 ==> x >= res

You're trying to prove res == 5 from this. The second of these three things immediately gives you half of that equality, so all you need to do is obtain 5 >= res. If you instantiate the quantifier with 5 for x, you will get

5 >= 4 && 5 >= 4 ==> 5 >= res

which simplifies to 5 >= res, which is what you need, so that's the end of your proof.

In summary, the proof comes down to instantiating the quantifier with 5 for x. Next, you need to know a little about how the Dafny verifier instantiates quantifiers. Essentially, it does this by looking at the "shape" of the quantifier and looking for similar things in the context of what you're trying to prove. By "shape", I mean things like "the functions and predicates it uses". Usually, this technique works well, but in your case, the quantifier is so plain that it doesn't have any "shape" to speak of. Consequently, the verifier fails to come up with the needed instantiation.

It would be nice if we could just say "hey, try instantiating that quantifier with 5 for x". Well, we can, if we give the quantifier some "shape" that we can refer to. That's what those wiki and other guidelines are trying to say. This is where it's useful to introduce the predicate greater. (Don't try to manually write trigger annotations.)

Alright, after introducing greater, your specification says

ensures greater(max, a, b)
ensures forall x :: greater(x, a, b) ==> x >= max

This says "max satisfies greater(max, a, b)" and "among all values x that satisfy greater(x, a, b), max is the smallest". After the call to Max in Main, we then have:

greater(res, 4, 5)
forall x :: greater(x, 4, 5) ==> x >= res

Recall, I said the verifier tries to figure out quantifier instantiations by looking at the quantifier and looking at the context around your assertion, and you're trying to instantiate the quantifier with 5 for x. So, if you can add something to the context just before the assertion that tempts the verifier to do that instantiation, then you're done.

Here's the answer: you want to introduce the term greater(5, 4, 5). This has a shape much like the greater(x, 4, 5) in the quantifier. Because of this similarity, the verifier will instantiate x with 5, which gives

greater(5, 4, 5) ==> 5 >= res

And since greater(5, 4, 5) is easily proved to be true, the needed fact 5 >= res follows.

So, change the body of Main to

var res := Max(4, 5);
assert greater(5, 4, 5);
assert res == 5;

and you're done. The verifier will prove the both assertions. The first is trivial, and after proving it, the verifier gets to use the term greater(5, 4, 5) in the proof of the second assertion. That term is what triggers the quantifier, which produces the fact 5 >= res, which proves the second assertion.

I want to point out that most quantifiers we try to prove do have some shape already. In your case, the predicate greater was introduced in order to give some shape to the quantifier. The technique of adding the extra assertion (here, assert greater(5, 4, 5)) is the same whether or not greater was already defined or was introduced as a trivial predicate that provides shape.

Upvotes: 1

Related Questions