Trivial Optimal and Correct Abstract interpretation

Beiträge: 179
Registriert: 15. Apr 2015 18:24

Trivial Optimal and Correct Abstract interpretation

Beitrag 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 :)

Zurück zu „Archiv“