Unrolling a predicate more than once

Nov 17, 2015 at 10:19 AM
Is there a way to ask Dafny to inline a recursively defined predicate some fixed number of times (more than once)?

I am able to do some static analysis on the program I am trying to verify, and I know that in order to verify the program a particular predicate must be unrolled at most some number of times, for example "at most 6 times".
Developer
Nov 17, 2015 at 4:40 PM
There's an experimental annotation called "fuel" that will let you do this. There are a lot of examples in Dafny's test directory in Test/dafny0/Fuel.dfy, but the basic idea is that you can write something like:
function {:fuel 3} pos(x:int) : int
{
    if x < 0 then 0
    else 1 + pos1(x - 1)
}
Which will tell Dafny/Z3 to unroll the definition three times. Note that this may lead to worse prover performance (or more time outs) since it will cause Z3 to do more work. You can also narrow the scope to a specific method or even statement. For example:
function pos(x:int) : int
{
    if x < 0 then 0
    else 1 + pos1(x - 1)
}

method {:fuel pos,3} test1(y:int) 
    requires y > 5;
{
    assert pos3(y) == 5 + pos3(y - 5);  // Just enough fuel to get here
}

method test2()
{
    assert {:fuel pos,3} pos3(y) == 5 + pos3(y - 5);  // Just enough fuel to get here
}
Note that we're still working through some issues with fuel, so there may be some changes in the next few months.
Marked as answer by lexicalscope on 12/1/2015 at 2:36 AM