Correção do programa, a especificação

Wikipedia: Na ciência teórica da computação, a correção de um algoritmo é afirmada quando se diz que o algoritmo está correto em relação a uma especificação.

Mas o problema é que obter a especificação "apropriada" não é uma tarefa trivial, e não existe um método 100% correto (tanto quanto eu saiba) para obter o método correto, é apenas uma estimativa, portanto, se vamos tome um predicado como uma especificação apenas porque "se parece" com o "um", por que não considerar o programa correto apenas porque "parece" correto?

Primeiro, você está absolutamente certo: você está realmente preocupado. A verificação formal transfere o problema de confiança na correção do programa para o problema de confiança na correção da especificação, portanto não é uma bala de prata.

Existem várias razões pelas quais esse processo ainda pode ser útil.

1. As especificações geralmente são mais simples que o próprio código. Por exemplo, considere o problema de classificar uma matriz de números inteiros. Existem algoritmos de classificação bastante sofisticados que fazem coisas inteligentes para melhorar o desempenho. Mas a especificação é bastante simples de declarar: a saída deve estar em ordem crescente e deve ser uma permutação da entrada. Assim, é sem dúvida mais fácil ganhar confiança na correção da especificação do que na correção do próprio código.

2. Não há um ponto único de falha. Suponha que você tenha uma pessoa que anote uma especificação e outra pessoa que escreva o código-fonte e depois verifique formalmente se o código atende à especificação. Então qualquer falha não detectada teria que estar presente em ambas as especificações e código. Em alguns casos, para alguns tipos de falhas, isso parece menos provável: é menos provável que você ignore a falha ao inspecionar as especificações e negligencie a falha ao inspecionar o código-fonte. Nem todos, mas alguns.

3. Especificações parciais podem ser muito mais simples que o código. Por exemplo, considere o requisito de que o programa esteja livre de vulnerabilidades de saturação de buffer. Ou, o requisito de que não haja erros fora dos limites do índice de matriz. Essa é uma especificação simples que é obviamente uma coisa boa e útil para poder provar. Agora você pode tentar usar métodos formais para provar que o programa inteiro atende a essa especificação. Essa pode ser uma tarefa bastante envolvida, mas se você for bem-sucedido, ganha mais confiança no programa.

4. As especificações podem mudar com menos frequência do que o código. Sem métodos formais, cada vez que atualizamos o código-fonte, precisamos verificar manualmente se a atualização não apresentará bugs ou falhas. Métodos formais podem potencialmente reduzir esse fardo: suponha que a especificação não seja alterada, de modo que as atualizações de software envolvam apenas alterações no código e não alterações na especificação. Então, para cada atualização, você fica isento do ônus de verificar se a especificação ainda está correta (ela não mudou, para que não haja risco de novos bugs terem sido introduzidos na especificação) e do ônus de verificar se o código ainda está correto (o verificador de programa verifica isso para você). Você ainda precisa verificar se as especificações originais estão corretas, mas não precisa verificar sempre que um desenvolvedor comete um novo patch / atualização / alteração.

Por fim, lembre-se de que as especificações geralmente são declarativas e não podem necessariamente ser executadas nem compiladas diretamente no código. Por exemplo, considere a classificação novamente: a especificação diz que a saída está aumentando e é uma permutação da entrada, mas não há uma maneira óbvia de "executar" essa especificação diretamente e nenhuma maneira óbvia de um compilador compilá-la automaticamente no código. Portanto, apenas pegar as especificações como corretas e executá-las com frequência não é uma opção.

No entanto, os resultados permanecem os mesmos: métodos formais não são uma panacéia. Eles simplesmente transferem o problema (muito difícil) de confiança na correção do código para o problema (apenas difícil) de confiança na correção da especificação. Os erros nas especificações são um risco real, são comuns e não podem ser ignorados. De fato, a comunidade de métodos formais às vezes separa o problema em duas partes: verificação significa garantir que o código atenda às especificações; validação é garantir que as especificações estejam corretas (atenda às nossas necessidades).

Você também pode aproveitar a verificação formal do programa na prática e por que não estamos pesquisando mais para garantir o tempo de compilação? para mais perspectivas com alguma influência nisso.

A resposta da DW é ótima , mas eu gostaria de expandir um ponto. Uma especificação não é apenas uma referência na qual o código é verificado. Uma das razões para ter uma especificação formal é validá-la, provando algumas propriedades fundamentais. Obviamente, a especificação não pode ser completamente validada - a validação seria tão complexa quanto a própria especificação, portanto seria um processo sem fim. Mas a validação nos permite obter uma garantia mais forte em algumas propriedades críticas.

Por exemplo, suponha que você esteja projetando um piloto automático de carro. Isso é bastante complexo, envolvendo muitos parâmetros. As propriedades de correção do piloto automático incluem coisas como "o carro não bate contra a parede" e "o carro dirige para onde é solicitado". Uma propriedade como “o carro não bate contra a parede” é realmente muito importante, então gostaríamos de provar isso. Como o sistema opera no mundo físico, você precisará adicionar algumas restrições físicas; a propriedade real do sistema computacional será algo como "sob essas suposições relacionadas à ciência dos materiais e essas suposições relativas à percepção de obstáculos pelos sensores do carro, o carro não colidirá com a parede". Mas, mesmo assim, o resultado é uma propriedade relativamente simples que é claramente desejável.

Você poderia provar essa propriedade a partir do código? Por fim, é isso que está acontecendo, se você seguir uma abordagem totalmente formal¹. Mas o código tem muitas partes diferentes; os freios, as câmeras, o motor etc. são todos controlados de forma autônoma. Uma propriedade de correção dos freios seria algo como "se o sinal 'aplicar freios' estiver ativado, os freios serão aplicados". Uma propriedade de correção do motor seria "se o sinal da embreagem estiver desligado, o motor não estará dirigindo as rodas". É preciso uma visão de alto nível para reuni-los. Uma especificação cria uma camada intermediária na qual os diferentes componentes do sistema podem ser articulados juntos.

De fato, um sistema tão complexo como o piloto automático de um carro teria vários níveis de especificações com quantidades variadas de aprimoramentos. Uma abordagem de refinamento é frequentemente usada no design: comece com algumas propriedades de alto nível, como “o carro não bate contra a parede”, depois descubra que isso requer sensores e freios e elabore alguns requisitos básicos para os sensores, os freios e o software piloto, refine novamente esses requisitos básicos no design do componente (para o sensor, vou precisar de um radar, um DSP, uma biblioteca de processamento de imagens, etc.) etc. Em um processo formal de desenvolvimento, comprovadamente, cada nível de especificação atende aos requisitos definidos pelo nível acima, desde as propriedades de nível mais alto até o código.

É impossível ter certeza de que a especificação está correta. Por exemplo, se você errou na física, os freios podem não ser eficazes, mesmo que a matemática que relaciona o código de freio aos requisitos formais esteja correta. Não é bom provar que as quebras são eficazes com 500 kg de carga se você realmente tiver 5000 kg. Mas é mais fácil ver que 500 kg estão errados do que ver dentro do código dos freios que eles não serão bons o suficiente para os parâmetros físicos do carro.

¹ _{O oposto de uma abordagem totalmente formal é "Acho que isso funciona, mas não tenho certeza". Quando você está apostando sua vida, isso não parece tão bom.}