Normally, in Dafny, a calc hides everything except the outermost relationship. For instance, after the following code:
calc {
    a;
    < { assert Property1(); } b;
    < { lemma2(); } c;
    <= { lemma3(); d;
}

Dafny remembers a < d but nothing else. However, DafnyCC doesn't quite forget everything else. It does forget all the stuff inside the intermediate explanations, e.g., it forgets the assertion of Property1() and it forgets all post-conditions of lemma2 and lemma3. However, it also remembers intermediate calc relationships. In the example above, those would be a < b, b < c, and c <= d.

This failure to forget can sometimes cause DafnyCC to know too many facts, and thus to time-out when trying to decide things. To get around this problem, you can nest the calc inside an outer calc that just proves the relationship you're interested in. For instance, for the above example, you could nest it as follows:
calc {
    a;
    <
     calc {
        a;
        < { assert Property1(); } b;
        < { lemma2(); } c;
        <= { lemma3(); d;
    }
    d;
}

Last edited Oct 14, 2014 at 11:12 PM by howell, version 1

Comments

No comments yet.