ti-enxame.com

As provas de correção de código algum dia se tornarão populares?

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

14
Casebash

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

Também programar para contratar pode ser útil. Consulte Contratos de código da Microsoft

8
Jonas

Todos, exceto os programas mais triviais

não pode ser totalmente comprovado como correto com 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 ser completa e correta. Normalmente, isso não é nada que você possa criar facilmente para a maioria dos programas do mundo real. Por exemplo, tente escrever uma especificação para algo como a interface do usuário deste site de discussão e você sabe o que quero dizer.

Aqui encontrei um bom artigo sobre o assunto:

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

14
Doc Brown

O problema com as provas formais é que elas apenas recuam um passo.

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ê especifica isso. E como você define o que o programa deve fazer em casos Edge que a especificação não cobre? Bem, então você tem que fazer as especificações mais detalhadas.

Então, digamos que sua especificação finalmente se torne detalhada o suficiente para descrever o comportamento correto de cada aspecto de todo o programa. Agora você precisa de uma maneira de fazer com que suas ferramentas de prova entendam isso. Então você tem que traduzir a especificação para algum tipo de linguagem formal que a ferramenta de prova possa entender ... ei, espere um minuto!

10
Mason Wheeler

A verificação formal já percorreu um longo caminho, mas geralmente as ferramentas da indústria/amplamente utilizadas estão 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 oferece suporte a contratos de código (pré/pós condições e invariantes) e pode usar esses contratos para fazer vários tipos de análise estática.

Projetos semelhantes a este existem para outras linguagens, como JML para Java, e Eiffel tem isso praticamente integrado.

Indo ainda mais longe, projetos como slam e blast podem ser usados ​​para verificar certas propriedades comportamentais com anotações/intervenções mínimas do programador, mas ainda não podem lidar com a generalidade total das linguagens modernas ( coisas como estouro de 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 as invariáveis ​​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.

8
Lucina

Não, a menos que apareça um método de provar o código automaticamente sem um extenso trabalho de desenvolvedor.

4
Fishtoaster

Tropecei nesta questão, e acho que este link pode ser interessante:

Aplicações Industriais da Astrée

Provar a ausência de RTE em um sistema usado pela Airbus com mais de 130 mil linhas de código em 2003 não parece ser ruim, e eu me pergunto se alguém vai dizer que este não é o mundo real.

3
zw324

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

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

Obviamente, desenvolver software com menos bugs é muito caro. Mas a abordagem do método formal faz sentido para algum tipo de software. Se você for 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 sujeito a erros).

3
Basile Starynkevitch

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.

Na verdade, a execução do código por meio de testes de unidade encontra essas coisas quase que imediatamente, e um conjunto coeso de testes negará a necessidade de quaisquer provas formais. Todos os casos de uso - bons, ruins, de erro e casos extremos - devem ser enumerados nos testes de unidade, que acabam sendo a melhor prova de que o código está correto do que qualquer prova separada do código.

Especialmente se os requisitos mudarem ou o algoritmo for atualizado para corrigir um bug - a prova formal tem mais probabilidade de ficar desatualizada, assim como os comentários de código costumam ficar.

2
Izkata

Eu acho 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 mainstream.

1
Paddyslacker

Já é usado por todos. Cada vez que você usa a verificação de tipo de sua linguagem de programação, está basicamente fazendo uma prova matemática da correção de seu programa. Isso já funciona muito bem - requer apenas que você escolha os tipos corretos para cada função e estrutura de dados que usar. Quanto mais preciso for o tipo, melhor será a verificação. Os tipos existentes disponíveis em linguagens de programação já possuem ferramentas poderosas o suficiente para descrever quase todos os comportamentos possíveis. 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 fazem isso quando o programa é executado. A verificação ainda existe em todas essas linguagens. (Para exemplo, c ++ já suporta a verificação de efeitos colaterais da mesma forma que o haskell, mas você só precisa escolher usá-lo.)

1
tp1