Dureza computacional de programas de computador "reais"

Ouvi muitas vezes dizer que você não pode escrever um programa para detectar bugs em um navegador da Web, processador de texto ou sistema operacional, por causa do Teorema de Rice: qualquer propriedade semântica para uma linguagem completa de Turing é indecidível.

No entanto, não sei até que ponto isso se aplica a programas do mundo real, como sistemas operacionais. Esses tipos de programas precisam de toda a força da integridade de Turing? Existem modelos mais simples de computação (como PR) nos quais esses aplicativos podem ser escritos? Em caso afirmativo, até que ponto isso permite decidir a correção do programa?

Você certamente pode escrever programas que detectam bugs - existe uma comunidade grande e ativa de pessoas que escrevem programas para fazer exatamente isso. No entanto, o que o teorema de Rice impede que você faça é escrever apanhadores de bugs que sejam ao mesmo tempo sólidos e completos (ou seja, pegar todos os bugs de uma determinada classe sem falsos positivos).

Dito isto, restrições ingênuas ao modelo de computação não ajudam muito a melhorar a praticidade da análise de programas. O motivo é que você pode obter programas que fazem "quase a mesma coisa" girando os loops enquanto

while P do 
   C

em for-loops com uma grande constante de iteração:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

Agora, esse programa nem precisa da força total da recursiva primitiva (já que o loop for pode ser macro-expandido em uma enorme declaração aninhada if-then-else), mas na maioria dos casos práticos, ele se comportará da mesma maneira que antes. Observe que isso ajuda a decidir na teoria - o programa é total, para que você possa responder a perguntas executando o programa e vendo o que acontece. Não é isso que realmente queremos, que é obter respostas mais rapidamente do que executar o programa - a terminação artificial introduzida na verdade não ajuda na análise do programa na prática, pois os erros ocorrem devido a erros na lógica real do programa, e nós não temos ' Não toquei nisso.

$\epsilon_0$

Como você perguntou sobre a correção de programas do mundo real, como sistemas operacionais, você pode estar interessado no projeto seL4 ( diário , pdf , conferência ).

A equipe do NICTA levou um microkernel de terceira geração de 8700 linhas de C e 600 linhas de montador implementadas de acordo com uma especificação abstrata em Haskell. Eles forneceram uma prova formal e verificada por máquina (em Isabelle / HOL) de que a implementação segue estritamente a especificação. Provando assim que o programa deles é livre de bugs.

Portanto, assim como o problema de parada, embora não possa ser resolvido em geral, ele pode ser resolvido para algumas instâncias específicas. Nesse caso, embora você não possa provar que o código C arbitrário está livre de erros, eles poderiam fazê-lo no caso do microkernel seL4.

As perguntas que você faz são realmente bem diferentes.

No entanto, não sei até que ponto isso se aplica a programas do mundo real, como sistemas operacionais. Esses tipos de programas precisam de toda a força da integridade de Turing?

É preciso muito pouco para um modelo de computação ser Turing completo. Por exemplo, vários modelos com contadores podem simular máquinas de Turing. Se você acredita que seu software requer mais de dois contadores que você pode manipular arbitrariamente, você está usando um idioma completo de Turing. Embora os números inteiros da máquina sejam delimitados a priori, as estruturas de dados alocadas em heap geralmente não são. Se o seu software precisar de listas, árvores e outros dados alocados dinamicamente, você estará usando um idioma completo do Turing.

Existem modelos mais simples de computação (como PR) nos quais esses aplicativos podem ser escritos? Em caso afirmativo, até que ponto isso permite decidir a correção do programa?

É importante reconhecer que não queremos verificar propriedades arbitrárias do nosso software. A verificação de propriedades estreitas e muito específicas (sem estouros de buffer, sem referência a ponteiro nulo, sem loops infinitos etc.) melhora imensamente a qualidade e a usabilidade do software. Em teoria, esses problemas ainda são indecidíveis. Na prática, o foco em propriedades específicas nos permite descobrir estruturas em nossos programas que podemos explorar com frequência para resolver o problema.

Em particular, você pode modificar sua pergunta original para

Existe uma abstração do meu software que eu possa analisar eficientemente em um modelo completo não-Turing?

Uma abstração é um modelo que inclui o comportamento do software original e possivelmente muitos comportamentos adicionais. Existem modelos como máquinas de balcão ou sistemas de empilhamento que não são completos para Turing e que podemos analisar. A abordagem padrão na verificação de programas com ferramentas automatizadas é construir uma abstração nesse modelo e verificá-la algoritmicamente.

Existem aplicativos em que as pessoas se preocupam com propriedades sofisticadas de seu hardware ou software. As empresas de hardware querem que seus chips implementem corretamente os algoritmos aritméticos, as empresas automotivas e aviônicas querem software com certificação correta. Se isso é importante, é melhor você usar um ser humano (treinado).