Regular Dafny can often infer inductive invariants, so you don't always have to state them. DafnyCC doesn't do this automatic inference, so you have to explicitly do the inductive assertions. Here's an illustrative example:

lemma AllIntegersAreKeen (j:int)
    ensures IntegerIsKeen(j);
{
    if j == 0 {
        lemma_ZeroIsKeen();
    }
    else {
        assert AllIntegersAreKeen(j-1);  // DafnyCC requires this explicit invocation
        lemma_KeennessForXImpliesKeennessForXPlusOne(j-1);
    }
}

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

Comments

No comments yet.