Incomplete odd/even abstraction rules in § 8 "Abstract Interpretation and Dataflow Analysis"

[mdempsky]

On page 44, there are rules for addition/subtraction/multiplication on odd/even/unknown values. However, the rules for "-" only give a precise answer for E - E, whereas it could use the same rules as "+" (i.e., giving precise answers for all of {E,O} x {E,O}).

The omission doesn't compromise the soundness of the abstraction, but it is at odds with the previous page describing the abstracted operators as "push[ing] abstraction through arithmetic operators, calculating their most precise abstractions."

It seems like either (1) the rules for "+" and "-" should match, or (2) the text could take the opportunity to point out that while "-" is less precise, it doesn't compromise its soundness.

[achlipala]

Does your characterization hold even though, in Coq, n - m = 0 when m > n?

[mdempsky]

Oops, I wasn't reading closely enough there. I suppose because of the introduction of -, I just assumed we were in Z. No, I do not think my characterization holds in N with Coq's subtraction rules---I withdraw that point. Sorry about that!

For what it's worth, it seems like § 7 introduces e - e, but doesn't define ⟦e - e⟧v.