Limites e Dificuldades no Design de Domínios Abstratos de Subaproximação

O principal objetivo da maioria das análises estáticas é provar a ausência de bugs: se a análise não reporta alarmes, então o programa não apresentará comportamentos indesejados. Por essa razão, elas são projetadas para superaproximar comportamentos de programa e, consequentemente, podem reportar alguns alarmes falsos. O trabalho recente de O’Hearn sobre incorreção renovou o interesse no uso de subaproximações para a detecção de bugs, porque elas apenas reportam alarmes verdadeiros. Em princípio, técnicas de Interpretação Abstrata podem lidar com subaproximações assim como com superaproximações, mas, na prática, poucas tentativas foram desenvolvidas para as primeiras, não obstante a literatura muito mais ampla sobre as últimas. Neste artigo, investigamos a possibilidade de explorar domínios abstratos de subaproximação para análises de detecção de bugs. Primeiro, restringimos a considerar domínios de potência concreta e destacamos algumas assimetrias intuitivas entre superaproximações e subaproximações. Em seguida, provamos que a eficácia de domínios abstratos definidos por conexões de Galois de Subaproximação é limitada, porque a análise provavelmente retornará resultados triviais sempre que funções de transferência comuns forem codificadas no programa. Para isso, introduzimos os conceitos originais de funções não vazias e uma família de funções altamente sobrejetivas e provamos a inexistência de domínios abstratos capazes de subaproximar tais funções de maneira não trivial. Mostramos muitos exemplos de domínios numéricos finitos e infinitos, bem como outros domínios genéricos. Em todos esses casos, provamos a impossibilidade de realizar análises não triviais por meio de conexões de Galois subaproximadoras.