Seite 1 von 1
Error in Sample Solution of Exercise 5.2
Verfasst: 6. Dez 2017 14:45
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:
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.
Re: Error in Sample Solution of Exercise 5.2
Verfasst: 3. Feb 2018 20:16
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