achlipala/frap

Inconsistent use of "most precise answer" on page 47

Closed this issue · 0 comments

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".