Inconsistent use of "most precise answer" on page 47
Closed this issue · 0 comments
mdempsky commented
At the end of section 8.2, it's claimed that "n -> Top" is the most precise answer for analyzing the doubling code. This is true if we're talking about abstract states valid at any point during execution, as n can be odd within the loop. But at termination, n will always be 0, so the most precise answer would be "n -> Even".
On the other hand, section 8.3 opens talking about how "x -> Odd" is the most precise answer for "x <- 0; x <- 1". But this only a sound answer if we're talking about analysis at termination, as opposed to any point during execution.
One way to resolve this inconsistency would be to qualify at the end of section 8.2 that flow-insensitive analysis "gives the most precise answer for x".