How does Dafny support induction if Z3 does not?

Question

Dafny has the option to set {:induction false}. Also, as far as I know, whenever we use assertions in Dafny, what happens below it that it constructs proof obligations and then calculates on them using Z3.

However, I read Z3 does not support induction: e.g., ... however, any non-trivial property will require a proof by induction. Z3 currently does not support proofs by induction... (cross product in z3)

So my question is: whenever we set {:induction true}, how is this induction performed in Dafny if not using Z3? Are there different underlying solvers? Are there any kind of heuristics? This last one is suggested here (Z3 model for correct Dafny method).

However, which type of heuristics are we talking about?

Answer 1

Maybe not as detailed as @alias' answer, but in short, Dafny's implicit {:induction true} attribute will add assumptions about sub-terms so that you don't need to write them yourself.

So if you write a recursive lemma to prove that every third Fibonacci number is even, without {:induction}, you have to invoke the lemmas recursively. Dafny will require also require recursive calls to terminate:

function fib(x: nat): nat {
  if x == 0 then 0 else
  if x == 1 then 1 else
  fib(x-1) + fib(x-2)
}

lemma {:induction false} FibIsDivisibleBy2(a: nat)
  ensures a % 3 == 0 <==> fib(a) % 2 == 0
{
  if a <= 2 {
  } else {
    FibIsDivisibleBy2(a-1);
    FibIsDivisibleBy2(a-2);
  }
}

Under the hood, the formula sent to Z3 for verification does not contain induction, but it will unroll fib using a fuel to bound unrolling, and the resulting formula will look like this ultra simplified and Dafny-pretending-to-be-SMT-LIB syntax:

(declare-fun a Int)
(declare-fun fib (Int) Int)

(assert forall fib[fuel+1](a) == fib[fuel](a))

(assert fib[n+1](a) == (if a == 0 then 0 else if a == 1 then 1 else fib[n](a))

(assert (
  || (a <= 2                        // First branch
      && !(     a % 3 == 0
         <==> fib[2](a) % 2 == 0)  // Postcondition, negated.
  || (a > 2
      &&   // We add the assumptions provided by the recursive calls to lemma:
      ( && ((a-1) % 3 == 0 <==> fib[1](a-1) % 2 == 0)
        && ((a-2) % 3 == 0 <==> fib[1](a-2)  % 2 == 0)
        && 
         !(a % 3 == 0 <==> fib[2](a) % 2 == 0)  /// Postcondition, negated
))))
(check-sat)

which z3 will return to be "unsat" without requiring induction. You can prove this formula by hand yourself, above. Note that I omit the mandatory check for the termination, which will look like 0 <= a - 1 < a && 0 <= a - 2 < a, and the subset type 0 <= a.

Now, if you add {:induction true}, what Dafny will do under the hood is to

• 1. Every time it sees another fib(X), it will instantiate the lemma automatically for you.
• 2. Unfold the definition of fib once and reapply 1) as needed.

That way, you don't need to write these recursive calls yourself and your lemma can prove with zero proof statements:

lemma {:induction true} FibIsDivisibleBy2(a: nat)
  ensures a % 3 == 0 <==> fib(a) % 2 == 0
{
}

Answer 2

Dafny is first a programming language, with built-in support for verification machinery of the programs you write. This machinery includes support for induction. Note that this has nothing to do with z3: It's something Dafny itself supports. So, to answer your question simply: Because Dafny's support for induction is not implemented by z3: It's implemented by Dafny itself. Compare this to the goal of z3: A push-button tool that understands SMTLib, excellent for applying decision procedures to (typically) quantifier-free subsets of first-order logic, algebraic data-types, reals, linear-integer arithmetic etc. In particular, z3 is not itself a programming language, nor it’s intended to be used in that way. This makes it suitable as a "backend" tool for custom tools like Dafny that focusses on specific programming styles.

The difficulty with induction is coming up with the inductive invariant. A good way to "guess" the invariant is to follow the structure of your program, which has been exploited to a great extent in the ACL2 theorem prover: The recursive nature of the program suggests an induction schema. Of course, this isn't always enough. The inductive hypothesis can be really difficult to come up with, and typically requires user guidance. This is the style used in most theorem provers, like HOL, Isabelle, Coq, Lean, and many others.

Looking back at Dafny, the need for induction typically comes from the loops in Dafny programs. (See: https://dafny.org/dafny/DafnyRef/DafnyRef#20141-loop-invariants-sec-loop-invariants). So, Dafny can construct the "inductive" proof by using the typical Hoare logic loop principle. (https://en.wikipedia.org/wiki/Hoare_logic) So, what Dafny does is takes your annotated program (and this is the key, you are expected to annotate loops with their invariants), sets up the inductive proof (i.e., the base-case and the inductive-step), and formulates those in terms of an SMTLib query and passes it to z3. (This is a simplified account, but it is roughly the strategy followed in similar tools like Why3 etc as well.) So, the "inductive" proof is done by Dafny, which keeps track of the proof status, how the subgoals for induction relate to each other and the overall goal etc., and z3 is merely used for establishing each of these individual goals that require no induction for their proofs.

A good paper to read on how Dafny works is Rustan's paper: Automating Theorem proving using SMT. This is a very good paper in the sense that it outlines how to build a theorem prover using SMT: While induction will be the main workhorse, there're many moving parts in such a system and Rustan gives a very nice overview of the techniques and challenges involved.

So, to summarize, Dafny supports induction because Dafny's verification system implements support for inductive proofs. z3 is simply a backend tool Dafny uses to discharge non-inductive goals; everything else is kept track of by Dafny itself.

Final note: Recent versions of SMTLib does include support for recursive-definitions, whose proofs will require induction. So, it is possible that SMT solvers will gain induction capabilities, and CVC5 already supports induction to some extent. (http://lara.epfl.ch/~reynolds/VMCAI2015-ind/smt-ind-RK.pdf). So, I'd expect more inductive capabilities to come to SMT-solvers in the upcoming years. However, tools like Dafny, ACL2, etc. will play a crucial role since coming up with inductive invariants is still an art more than engineering for most software applications; so user-intervention is still the name of the game. But it's reasonable to expect the automated systems to get better over time, as amply demonstrated by the last 50 years of theorem proving literature.