CodePlexProject Hosting for Open Source Software

1

Closed

Dafny performs some rewrites in an

The bug is that if

I imagine that the code currently does something like:

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

Thanks,

Rustan

`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

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)
}
}
```

No files are attached

## comments