As provas de correção do código sempre serão comuns? [fechadas]

14

Todos os programas, exceto os mais triviais, estão cheios de bugs e, portanto, qualquer coisa que promova removê-los é extremamente atraente. No momento, as provas de correção são um código extremamente esotérico, principalmente por causa da dificuldade de aprender isso e do esforço extra necessário para provar que um programa está correto. Você acha que a prova de código decolará?

programming-practices Casebash
fonte

Respostas:

8

Não exatamente nesse sentido, mas a programação funcional pura é boa nesse domínio. Se você usa o Haskell, é provável que o seu programa esteja correto se o código for compilado. Exceto no IO, um bom sistema de tipos é uma boa ajuda.

Também a programação do contrato pode ser útil. Consulte Contratos de código da Microsoft

Jonas
fonte
6
Desculpe - não fiz muito Haskell do "mundo real", mas já fiz exercícios tutoriais suficientes por várias vidas. Só porque ele compila não significa que é provável que funcione. Comparado com, por exemplo, Ada (escolhido por ser uma linguagem imperativa estritamente estaticamente tipificada), eu diria que Haskell é um pouco mais fácil, mas principalmente porque é mais conciso (menor complexidade ciclomática). Ao lidar com a mônada de IO, há aborrecimentos que podem tornar Haskell mais difícil de acertar - é apenas diferente o suficiente do estilo imperativo que existem coisas que não podem ser feitas naturalmente.
Steve314
Em "não é possível fazer o que é natural", considere um loop "while". Sim, você pode rodar sozinho - mas a condição while deve estar dentro da mônada, pois precisa reagir aos efeitos colaterais do corpo do loop. Isso não significa apenas que você recebeu permissão para causar efeitos colaterais na condição while, mas também torna difícil o uso desse loop while. Resultado final - geralmente é mais fácil usar a recursão mesmo no código de Mônada IO - e isso significa que você precisa estruturar as coisas de uma maneira específica.
Steve314
14

Todos, exceto os programas mais triviais

não pode ser totalmente comprovado como correto com um esforço razoável. Para qualquer prova formal de correção, você precisa de pelo menos uma especificação formal, e essa especificação deve estar completa e correta. Isso normalmente não é nada que você possa criar facilmente para a maioria dos programas do mundo real. Por exemplo, tente escrever essa especificação para algo como a interface do usuário deste site de discussão e você entende o que quero dizer.

Aqui encontrei um bom artigo sobre o tema:

http://www.encyclopedia.com/doc/1O11-programcorrectnessproof.html

Doc Brown
fonte
Certo - para qualquer projeto de programação, há uma transição de uma descrição informal do problema para uma formal (normalmente, hoje, na forma de um programa), e isso não desaparece.
David Thornley
astree.ens.fr Veja aqui as aplicações industriais da Astrée
zw324
@ZiyaoWei: essas ferramentas são úteis, mas encontram apenas alguns erros formais, não mais. Se um programa de uma linha como printf("1")está correto ou não (por exemplo, porque o requisito era "imprimir um número aleatório igualmente distribuído de 1 a 6") não pode ser decidido por um analisador estático.
Doc Brown
10

O problema das provas formais é que ele apenas retrocede o problema.

Dizer que um programa está correto é equivalente a dizer que um programa faz o que deve fazer. Como você define o que o programa deve fazer? Você o especifica. E como você define o que o programa deve fazer em casos extremos que as especificações não cobrem? Bem, então você precisa tornar as especificações mais detalhadas.

Então, digamos que suas especificações finalmente se tornem detalhadas o suficiente para descrever o comportamento correto de todos os aspectos de todo o programa. Agora você precisa de uma maneira de fazer com que suas ferramentas de prova entendam. Então você tem que traduzir as especificações em algum tipo de linguagem formal que a ferramenta de provas possa entender ... ei, espere um minuto!

Mason Wheeler
fonte
2
Também .. "Cuidado com os bugs no código acima; eu apenas provei que está correto, não tentei." - Donald Knuth
Brendan
8

A verificação formal já percorreu um longo caminho, mas geralmente as ferramentas amplamente utilizadas pela indústria / setor ficam atrás das pesquisas mais recentes. Aqui estão alguns esforços recentes nessa direção:

Spec # http://research.microsoft.com/en-us/projects/specsharp/ Esta é uma extensão do C # que suporta contratos de código (condições pré / pós e invariantes) e pode usar esses contratos para fazer vários tipos de análise estática .

Projetos semelhantes a esse existem para outros idiomas, como o JML para java, e o Eiffel tem esse recurso embutido.

Indo além, projetos como slam e blast podem ser usados ​​para verificar determinadas propriedades comportamentais com anotação / intervenção mínima do programador, mas ainda não conseguem lidar com a generalidade total das linguagens modernas (coisas como excesso de número inteiro / aritmética de ponteiro não são modeladas).

Acredito que veremos muito mais dessas técnicas usadas na prática no futuro. A principal barreira é que os invariantes do programa são difíceis de inferir sem anotações manuais, e os programadores geralmente não estão dispostos a fornecer essas anotações porque isso é muito tedioso / demorado.

Lucina
fonte
4

A menos que surja um método para provar automaticamente o código sem um extenso trabalho do desenvolvedor.

Fishtoaster
fonte
Considere o argumento econômico: talvez seja melhor para os desenvolvedores "desperdiçar" tempo com provas de correção do que perder dinheiro por causa de erros de software.
187 Andres F.
Concordo com a fishtoaster, a menos que se torne muito menos intensivo em recursos, uma grande quantidade de software comercial regular simplesmente não terá o custo / benefício para suportar esse nível de correção. Em um aplicativo de LOB para um público cativo, por vezes, o benefício de negócios mais para o custo em relação a um relatório de bug é a adição de uma linha para os docs que diz "não faça isso"
Bill
3

Algumas ferramentas formais de métodos (como, por exemplo, o Frama-C para software C crítico incorporado) podem ser vistas como (mais ou menos) fornecer, ou pelo menos verificar, uma prova (de correção) de um determinado software. (O Frama-C verifica se um programa obedece à sua especificação formalizada, em algum sentido, e respeita os invariantes explicitamente anotados no programa).

Em alguns setores, esses métodos formais são possíveis, por exemplo, o DO-178C para software crítico em aeronaves civis. Portanto, em alguns casos, essas abordagens são possíveis e úteis.

Obviamente, desenvolver um software com menos bugs é muito caro. Mas a abordagem do método formal faz sentido para algum tipo de software. Se você é pessimista, pode pensar que o bug foi movido do código para sua especificação formal (que pode ter alguns "bugs", porque formalizar o comportamento pretendido de um software é difícil e propenso a erros).

Basile Starynkevitch
fonte
3

Eu me deparei com essa questão e acho que esse link pode ser interessante:

Aplicações Industriais da Astrée

Provar a ausência do RTE em um sistema usado pela Airbus com mais de 130 mil linhas de código em 2003 não parece ruim, e imagino que haverá alguém dizendo que esse não é o mundo real.

zw324
fonte
2

Não. O provérbio comum para isso é: "Em teoria, teoria e prática são iguais. Na prática, não".

Um exemplo muito simples: erros de digitação.

Realmente, executar o código através de testes de unidade encontra essas coisas quase imediatamente, e um conjunto coeso de testes negará a necessidade de quaisquer provas formais. Todos os casos de uso - casos bons, ruins, de erro e de borda - devem ser enumerados nos testes de unidade, que acabam como prova melhor de que o código está correto do que qualquer prova separada do código.

Especialmente se os requisitos forem alterados ou o algoritmo for atualizado para corrigir um erro - a prova formal tem mais probabilidade de ficar desatualizada, da mesma forma que os comentários de código costumam ter.

Izkata
fonte
3
Errado. Nenhum teste de unidade será capaz de cobrir toda a gama de parâmetros possíveis. Imagine "teste de unidade" um compilador dessa maneira, certificando-se de que nenhuma aprovação passe na semântica.
SK-logic
3
teste de unidade não é o santo graal ...
Ryathal 22/12
1
@Winston Ewert, existem compiladores verificados (e muitos mais montadores verificados). E o hardware é formalmente verificado com muito mais frequência do que o software. Veja aqui: gallium.inria.fr/~xleroy/publi/compiler-certif.pdf
SK-logic
1
@ SK-logic, sim, existem compiladores de brinquedo comprovadamente corretos para fins acadêmicos. Mas e os compiladores que as pessoas realmente usam? Suspeito que a maioria dos compiladores seja verificada usando várias formas de teste automatizado e quase nenhuma prova formal é feita.
Winston Ewert
1
@Winston Ewert, as provas de correção são práticas e amplamente utilizadas na vida real. O que não é muito prático é a maioria das linguagens tradicionais modernas. Espero que todos desapareçam, para que o valor das provas de correção aumente no futuro.
SK-logic
1

Penso que os limites impostos às provas de correção por causa do problema de parada podem ser a maior barreira para que as provas de correção se tornem comuns.

Paddyslacker
fonte
8
O problema da parada diz que não podemos determinar se algum programa arbitrário é interrompido. Esses programas podem fazer coisas estranhas, como testar todos os números inteiros para ver se é um primo de Mersenne. Não fazemos isso em programas normais!
Casebash
1
@ Casebash, a questão é se existe um subconjunto útil de programas para os quais o problema de parada pode ser resolvido. Isso não é de forma alguma claro. Ou seja, podemos restringir nossos programas para que não possamos fazer coisas como testar todos os números inteiros sem arruinar nossa capacidade de realizar tarefas úteis?
Winston Ewert
1

Já é usado por todos. Toda vez que você usa a verificação de tipo da sua linguagem de programação, está basicamente fazendo uma prova matemática da correção do seu programa. Isso já funciona muito bem - requer apenas a escolha de tipos corretos para cada função e estrutura de dados que você usar. Quanto mais preciso for o tipo, melhor será a verificação. Os tipos existentes disponíveis nas linguagens de programação já possuem ferramentas poderosas o suficiente para descrever praticamente qualquer comportamento possível. Isso funciona em todos os idiomas disponíveis. C ++ e as linguagens estáticas estão apenas fazendo as verificações em tempo de compilação, enquanto linguagens mais dinâmicas, como python, estão fazendo isso quando o programa é executado. A verificação ainda existe em todos esses idiomas. (por exemplo, o c ++ já suporta a verificação de efeitos colaterais da mesma forma que haskell,

tp1
fonte
Com o pouco sobre efeitos colaterais em C ++, você está se referindo à correção const?
Winston Ewert
sim, função de membro const + const. Se todas as suas funções de membro forem const, todos os dados nos objetos não serão modificáveis.
tp1
Eles ainda podem ser modificados se você usar mutableou const_cast. Eu certamente vejo a conexão que você desenha lá, mas o sabor de duas abordagens parece bastante diferente para mim.
Winston Ewert
Bem, é por isso que você precisa usá-lo - sempre há maneiras de contorná-lo. Mas o mais importante é como fazer os compiladores verificarem problemas na área.
tp1