Seite 1 von 1

Trivial Optimal and Correct Abstract interpretation

Verfasst: 27. Nov 2017 18:01
von 0b101101101

In the tasks we were twice asked to give an abstract interpretation that is correct and optimal. I've been wondering since, why the 'trivial' abstract interpretation, which simply returns a constant list of nones does not suffice:

fs : L→L
fs(m1,m2,m3, ...) = (none, none, none, ...)

Both the definitions of correctness and optimalness have a foreach condition on the value (sigma) in the lattice (m). As there are no values in none, the trivial abstract interpretation should thus be correct and optimal.

Do my thoughts make sense?

EDIT: Ah, forget it. I'll try to write a better question later :)