Perguntas sobre métodos e técnicas para provar a correção de programas.
Como engenheiro de software, escrevo muitos códigos para produtos industriais. Coisas relativamente complicadas com classes, threads, alguns esforços de design, mas também alguns compromissos de desempenho. Eu faço muitos testes e estou cansado de testar, então fiquei interessado em ferramentas...
Esta questão foi migrada do Theoretical Computer Science Stack Exchange porque pode ser respondida no Computer Science Stack Exchange. Migrou há 7 anos . "Alan Turing provou em 1936 que um algoritmo geral para resolver o problema de parada de todos os pares possíveis de...
Como você verifica se dois algoritmos (por exemplo, classificação de mesclagem e classificação Naïve) retornam o mesmo resultado para qualquer entrada, quando o conjunto de todas as entradas é infinito? Atualização: Obrigado Ben por descrever como isso é impossível de ser feito algoritmicamente no...
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...
Adoro tudo o que é tempo de compilação e adoro a idéia de que, depois que você compila um programa, muitas garantias são feitas sobre sua execução. De um modo geral, um sistema de tipo estático (Haskell, C ++, ...) parece oferecer garantias mais fortes em tempo de compilação do que qualquer sistema...
Na discussão em torno dessa questão , Gilles menciona corretamente que qualquer prova de correção de um algoritmo que utiliza matrizes deve provar que não há acesso a matrizes fora dos limites; dependendo do modelo de tempo de execução, isso causaria um erro de tempo de execução ou acesso a...
Quero fornecer provas para partes de um programa Haskell que estou escrevendo como parte de minha tese. Até agora, porém, não consegui encontrar um bom trabalho de referência. O livro introdutório de Graham Hutton, Programming in Haskell ( Google Books ) - que li enquanto aprendia Haskell - aborda...
Estou tentando me ensinar diferentes abordagens à verificação de software. Eu li alguns artigos. Até onde eu aprendi, a lógica proposicional com temporal geralmente usa verificação de modelo com solucionadores SAT (em sistemas reativos contínuos), mas e a lógica de primeira ordem com temporal? Ele...
Sobre o problema do Heartbleed, Bruce Schneier escreveu em seu Crypto-Gram de 15 de abril: '"Catastrófico" é a palavra certa. Na escala de 1 a 10, esse é um 11. ' Li vários anos atrás que um núcleo de um determinado sistema operacional foi rigorosamente verificado com um sistema de verificação de...
Seja e sejam vetores de variáveis booleanas. Eu tenho um predicado booleano em . Dou à minha amiga Priscilla . Em resposta, ela me fornece , um predicado booleano em , e ela afirma
Eu sei que a Verificação Simbólica de Modelo é uma travessia de espaço de estado com base em representações de conjuntos de estados e relações de transição como fórmulas, como em CTL, usando modelos como o Modelo Kripke. Eu conheço a teoria. Mas acho difícil entender a aplicação real. Onde...
A análise de fluxo de dados funciona sobre um gráfico de fluxo de controle. Quando um idioma em consideração suporta exceções, o gráfico de fluxo de controle pode explodir. Quais são as técnicas padrão para lidar com essa explosão? Podemos ignorar profundamente as arestas induzidas pela exceção?...
Eu sei que existe algo chamado correção parcial, mas eu queria saber se havia uma maneira de saber quão próximo um programa semi-correto está de um programa totalmente correto. Por exemplo, se você tivesse um programa de classificação que classifique quase completamente uma matriz, poderia usar a...