This project is read-only.
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 {
    else {
        assert AllIntegersAreKeen(j-1);  // DafnyCC requires this explicit invocation

Last edited Oct 15, 2014 at 12:11 AM by howell, version 1


No comments yet.