Por Gary Stix
Scientific American – janeiro/2007

Alan Turing , matemático e um dos fundadores da ciência da computação, demonstrou em 1936 ser impossível criar um algoritmo que garanta a qualquer programa que ele seja sempre executado até o final. A essência de seu argumento é que tal algoritmo sempre pode falhar ao analisar a si mesmo e descobrir que não consegue parar. “Isso leva a um paradoxo lógico”, afirma David Schimdt, professor da ciência da computação da Universidade Esadual do Kansas. Do ponto de vista prático, a incapacidade de “terminar”, segundo jargão da informática, é muito familiar a qualquer usuário do sistema operacional Windows, que clica num botão e fica olhando indefinidamente para o ícone da ampulheta, o qual indica que o programa entrou numa rotina (looping) interminável pelas mesmas linhas de código.

A versão atual do sistema operacional da Microsoft, conhecida como XP, é mais estável que as anteriores, mas os fabricantes de impressoras, tocadores de MP3 e outros dispositivos ainda produzem softwares de controles (drivers) falhos, que permitem um perfirérico interagir com o sistema operacional. Assim, a ampulheta “travada” continua familiar aos usuários do XP. O setor de pesquisas da Microsoft tentou recentemente solucionar esse problema interminável, concentrando-se em ferramentas que verificam se os drivers não contém defeitos ou bugs.

A Microsoft Research ainda não conseguiu contradizer Turing, mas começou a apresentar estudos em conferências sobre uma ferramenta chamada Terminator, que pretende garantir que um driver irá terminar o que está fazendo. os cintistas da computação não conseguiram, até agora, criar um verificador automático prático para a finalização (ou terminação) dos grandes programas em razão do fantasma de Turing, declara Byron Cook, cientista da computação do laboratório da Microsoft Research em Cambridge, Inglaterra, que comandou o projeto. “Turing provou que o problema é indecidível e isso de certa forma assustou as pessoas”, diz.

Misturando várias técnicas anteriores de análise automatizada de programas, o Terminator cria uma representação finita de um número infinito de estados em que um driver pode se encontrar enquanto executa um programa. Ele então tenta derivar um argumento lógico que mostre que o software irá terminar a tarefa. Isso é feito combinando várias “funções de classificação”, que medem quanto o driver progrediu no looping do programa – seqüências de instruções que se repetem até que uma condição específica seja atingida. O Terminator começa com um argumento inicial razoavelmente fraco, que ele aprimora de forma repetida, com base nas informações recebidas das tentativas falhas anteriores, para criar uma prova (um argumento sufientemente forte). O procedimento pode consumir horas em um poderoso computador até que, se tudo correr de acordo com os planos, surge uma prova de que não haverá atalhos de execução no driver capazes de causar a temida permanência da ampulheta.

Enquanto tenta obter uma prova, o Terminator, que está em operação há apenas nove meses e ainda deverá ser distribuído aos profissionais externos que desenvolvem drivers para Windows, conseguiu encontrar algumas falhas de finalização nos drivers a serem utilizados na futura versão do Windows Vista. Cook prevê que, no futuro, o Terminator deverá encontrar provas para 99,9% dos programas comerciais que terminam sua execução (é claro que há programas desenhados para serem executados indefinidamente). No entanto, Turing ainda pode descansar em paz. “Sempre haverá um programa que o Terminator não poderá provar que termina”, diz Cook. “Mas, se for possível fazê-lo funcionar em qualquer programa no mundo real, então isso não tem importância”.

Patrick Cousot, da Escola Normal Superior em Paris, um pioneiro em análises de programas matemáticos, destaca que o Terminator somente deve funcionar em um conjunto limitado de aplicações bem definidas. “Eu duvido que ele seja capaz de lidar com problemas de terminações matemáticas difíceis” – aqueles para números de ponto flutuante ou para programas executados ao mesmo tempo. Cook não discorda, dizendo que planeja desenvolver também métodos da prova de terminação para tais programas. No entanto, encontrar uma forma de garantir que programas mais complexos não travem é um desafio tão grande, segundo Cook, irá consumir o resto de sua carreira.