Seite 1 von 1

Error in Sample Solution of Exercise 5.2

Verfasst: 6. Dez 2017 14:45
von AlexanderF
hello,

Exercise 5.2 a) requires the abstract interpretation functions for assignments to be optimal.

I think the given functions for assignments S1 and S2 in the sample solution are not optimal.
For example for f_S1, there is a more informative function f'_S1 (f_S1 is not at least as informative as f'_S1)
which is defined like f_S1,
but f'_S1(l)(y) = none if l(y) = none.
f'_S1 is also correct with respect to the representation function beta:
Since
beta(sigma)(y) [= l(y) = none
cannot be satisfied (none is not in the image of beta), we do not need to consider whether
pos = beta(sigma_res)(y) [= f'_S1(l)(y) = none
is satisfied or not.

Best regards,
Alexander

Re: Error in Sample Solution of Exercise 5.2

Verfasst: 3. Feb 2018 20:16
von ximl
Hi Alexander,

Thanks for pointing out the non-optimality of f_S1 and f_S2.
In the this solution, each of f_S1, f_S2, f_S4 and f_S5 was
in fact non-optimal. For S1, the optimal analysis f_S1 is such that
f_S1(l) is the bottom element of L as long as one of l(x), l(y) and
l(z) is none, and f_S(l) is the same as in this solution otherwise.
This is because as long as one of l(x), l(y) and l(z) is none,
it is already impossible to find a state that is mapped to some l'
that is less than or equal to l under \beta (as in the definition of
the correctness of abstract interpretations). The solution has been
updated correspondingly.

Best regards,
Ximeng