A Análise Estática Não Pode Provar Que Seu Avião Não Vai Cair. Ela Pode Provar Algo Mais Útil.
A interpretação abstrata superaproxima todo estado possível do programa. Se uma divisão por zero é inalcançável na abstração, ela é inalcançável no código real. Veja como funciona e onde deixa de funcionar.
A análise estática não pode provar que um avião não vai cair. Ela pode provar que o loop de controle do altímetro nunca vai dividir por zero, nunca vai acessar…