1

Closed

Specialized predicates should include mutually recursive predicates

description

Dafny performs some rewrites in an inductive lemma and in a colemma. This bug report pertains to the rewrite that is being done with the "focus predicates" (aka "specialized predicates") of the inductive lemma or colemma. A focus predicate for an inductive lemma is an inductive predicate that occurs in the lemma's precondition; a focus predicate for a colemma is a copredicate that occurs in the lemma's postcondition. If an inductive/co-lemma is specialized for an inductive/co-predicate P, then in the body of the lemma, Dafny will rewrite calls to P into calls to P#[_k-1].

The bug is that if P is found to be a focus predicate, then all other inductive/co-predicates in P's strongly connected component (that is, all inductive/co-predicates that are mutually recursive with P) should also be included as focus predicates.

I imagine that the code currently does something like:
  • Find the set S of focus predicates in the lemma's pre- or postcondition.
  • NEW STEP TO FIX THE BUG: For every inductive/co-predicate P in S, add to S all inductive/co-predicates in the same strongly connected component (in the call graph) as P
  • Add a hover text to the lemma, saying "specialized for ...members of S..."
  • Do the rewrite in the body of the lemma
I imagine that three of these steps are already done (probably in the order I described), but the "NEW STEP" needs to be implemented. Once that step is implemented, I think the hover text and the rewriting should not need any further change.

In the test examples I'm including below, there are currently four places where verification errors occur. I expect that fixing the bug in the way I just described will cause everything to verify in this test file. (I don't know if the bug fix perhaps causes other things to break in the test suite; if so, let's talk if there's any confusion.) Optionally, the .expect file for this new test file could turn on /printTooltips, so that the test also shows the "specialized for ..." text.

Thanks,
Rustan
module InductiveThings {
  predicate P(x: int)
  predicate Q(x: int)

  inductive predicate A(x: int)
  {
    P(x) || B(x+1)
  }

  inductive predicate B(x: int)
  {
    Q(x) || A(x+1)
  }

  inductive lemma AA(x: int)  // should be specialized not just for A, but also for B, which is in the same strongly connected component as A in the call graph
    requires A(x)
  {
    if B(x+1) {  // this one should be replaced by B#[_k-1](x+1)
      BB(x+1);
    }
  }

  inductive lemma BB(x: int)  // should be specialized not just for B, but also for A, which is in the same strongly connected component as B in the call graph
    requires B(x)
  {
    if A(x+1) {  // this one should be replaced by A#[_k-1](x+1)
      AA(x+1);
    }
  }
}

module CoThings {
  copredicate A(x: int)
  {
    B(x+1)
  }

  copredicate B(x: int)
  {
    A(x+1)
  }

  colemma AA(x: int)  // should be specialized not just for A, but also for B, which is in the same strongly connected component as A in the call graph
    ensures A(x)
  {
    BB(x+1);
    assert B(x+1);  // this one should be replaced by B#[_k-1] (which will happen, provided that AA is listed as also being specialized for B)
  }

  colemma BB(x: int)  // should be specialized not just for B, but also for A, which is in the same strongly connected component as B in the call graph
    ensures B(x)
  {
    AA(x+1);
    assert A(x+1);  // this one should be replaced by A#[_k-1] (which will happen, provided that BB is listed as also being specialized for A)
  }
}
Closed Jun 16, 2016 at 8:52 PM by qunyanm

comments