Lógica Hoare - Hoare logic
A lógica Hoare (também conhecida como lógica Floyd-Hoare ou regras Hoare ) é um sistema formal com um conjunto de regras lógicas para raciocinar rigorosamente sobre a correção de programas de computador . Foi proposto em 1969 pelo cientista da computação e lógico britânico Tony Hoare , e posteriormente refinado por Hoare e outros pesquisadores. As ideias originais foram semeadas pelo trabalho de Robert W. Floyd , que publicou um sistema semelhante para fluxogramas .
Hoare triplo
A característica central da lógica Hoare é o triplo Hoare . Um triplo descreve como a execução de um trecho de código altera o estado da computação. Um triplo Hoare é da forma
onde e são afirmações e é um comando . é chamado a condição prévia e a pós-condição : quando a condição for atendida, a execução do comando estabelece a pós-condição. Asserções são fórmulas na lógica de predicados .
A lógica Hoare fornece axiomas e regras de inferência para todas as construções de uma linguagem de programação imperativa simples . Além das regras para a linguagem simples no artigo original de Hoare, regras para outras construções de linguagem foram desenvolvidas desde então por Hoare e muitos outros pesquisadores. Existem regras para concorrência , procedimentos , saltos e ponteiros .
Correção parcial e total
Usando a lógica Hoare padrão, apenas a correção parcial pode ser comprovada, enquanto a terminação precisa ser comprovada separadamente. Assim, a leitura intuitiva de um triplo de Hoare é: Sempre que mantém o estado antes da execução de , então o mantém depois ou não termina. No último caso, não há "depois", então pode haver qualquer afirmação. Na verdade, pode-se escolher ser falso para expressar que não termina.
A correção total também pode ser comprovada com uma versão estendida da regra While.
Em seu artigo de 1969, Hoare usou uma noção mais restrita de término que também implicava a ausência de quaisquer erros de tempo de execução: "A falha em terminar pode ser devido a um loop infinito; ou pode ser devido à violação de um limite definido pela implementação, para por exemplo, o intervalo de operandos numéricos, o tamanho do armazenamento ou um limite de tempo do sistema operacional. "
Regras
Esquema de axioma de declaração vazia
A regra de instrução vazia afirma que a instrução skip não altera o estado do programa, portanto, tudo o que for verdadeiro antes de pular também será verdadeiro depois.
Esquema de axioma de atribuição
O axioma de atribuição afirma que, após a atribuição, qualquer predicado que era anteriormente verdadeiro para o lado direito da atribuição agora é válido para a variável. Formalmente, seja P uma asserção em que a variável x é livre . Então:
onde indica a afirmação P em que cada ocorrência livre de X foi substituído pela expressão de E .
Os meios esquema de atribuição axioma que a verdade de que equivale à verdade depois-atribuição de P . Assim, fossem verdadeiras antes da atribuição, pelo axioma da atribuição, então P seria verdadeiro após a qual. Por outro lado, se forem falsos (ou seja, verdadeiros) antes da declaração de atribuição, P deve ser falso posteriormente.
Exemplos de triplos válidos incluem:
Todas as pré-condições que não são modificadas pela expressão podem ser transportadas para a pós-condição. No primeiro exemplo, a atribuição não altera o fato de que , portanto, ambas as afirmações podem aparecer na pós-condição. Formalmente, esse resultado é obtido aplicando-se o esquema axiomático com P sendo ( e ), que resulta em ser ( e ), que por sua vez pode ser simplificado para a pré-condição dada .
O esquema do axioma de atribuição é equivalente a dizer que, para encontrar a pré-condição, primeiro pegue a pós-condição e substitua todas as ocorrências do lado esquerdo da atribuição pelo lado direito da atribuição. Tenha cuidado para não tentar fazer isso ao contrário, seguindo esta maneira incorreta de pensar :; esta regra leva a exemplos absurdos como:
Outra regra incorreta que parece tentadora à primeira vista é ; isso leva a exemplos absurdos como:
Enquanto uma determinada pós-condição P determina exclusivamente a pré-condição , o inverso não é verdadeiro. Por exemplo:
- ,
- ,
- , e
são instâncias válidas do esquema de axioma de atribuição.
O axioma de atribuição proposto por Hoare não se aplica quando mais de um nome pode referir-se ao mesmo valor armazenado. Por exemplo,
é errado se x e y se referem à mesma variável ( aliasing ), embora seja uma instância adequada do esquema de atribuição axioma (com ambos e sendo ).
Regra de composição
Verificando o código de troca sem variáveis auxiliares |
||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
A regra de composição de Hoare se aplica a programas executados sequencialmente S e T , onde S é executado antes de T e é escrito ( Q é chamado de condição intermediária ):
Por exemplo, considere as duas seguintes instâncias do axioma de atribuição:
e
Pela regra de sequenciamento, conclui-se:
Outro exemplo é mostrado na caixa à direita.
Regra condicional
A regra condicional afirma que uma pós-condição Q comum a then e else part também é uma pós-condição da instrução if ... endif inteira . Na parte then e na outra parte, a condição B não negada e não negada pode ser adicionada à pré-condição P , respectivamente. A condição, B , não deve ter efeitos colaterais. Um exemplo é dado na próxima seção .
Esta regra não estava contida na publicação original de Hoare. No entanto, uma vez que uma declaração
tem o mesmo efeito que uma construção de loop único
a regra condicional pode ser derivada das outras regras de Hoare. De maneira semelhante, as regras para outras construções de programa derivadas, como loop for , do ... until loop, switch , break , continue podem ser reduzidas pela transformação do programa para as regras do artigo original de Hoare.
Regra de conseqüência
Esta regra permite fortalecer a pré-condição e / ou enfraquecer a pós-condição . É usado, por exemplo, para obter pós-condições literalmente idênticas para a parte then e the else .
Por exemplo, uma prova de
precisa aplicar a regra condicional, que por sua vez exige provar
- , ou simplificado
para a parte então , e
- , ou simplificado
para a outra parte.
No entanto, a regra de atribuição para a parte then requer a escolha de P como ; aplicação de regra, portanto, produz
- , que é logicamente equivalente a
- .
A regra de conseqüência é necessária para fortalecer a pré-condição obtida da regra de atribuição para a necessária para a regra condicional.
Da mesma forma, para a outra parte, a regra de atribuição produz
- , ou equivalente
- ,
portanto, a regra de conseqüência deve ser aplicada com e sendo e , respectivamente, para fortalecer novamente a pré-condição. Informalmente, o efeito da regra de consequência é "esquecer" o que é conhecido na entrada da parte else , uma vez que a regra de atribuição usada para a parte else não precisa dessa informação.
Enquanto regra
Aqui P é o invariante de laço , que é para ser preservado pelo corpo do loop S . Após o término do loop, esse P invariante ainda se mantém e, além disso, deve ter causado o término do loop. Como na regra condicional, B não deve ter efeitos colaterais.
Por exemplo, uma prova de
pela regra enquanto exige provar
- , ou simplificado
- ,
que é facilmente obtido pela regra de atribuição. Finalmente, a pós-condição pode ser simplificada para .
Para outro exemplo, a regra while pode ser usada para verificar formalmente o seguinte programa estranho para calcular a raiz quadrada exata x de um número arbitrário a - mesmo se x for uma variável inteira e a não for um número quadrado:
Depois de aplicar a regra while com P sendo verdadeiro , resta provar
- ,
que segue da regra de pular e da regra de consequência.
Na verdade, o programa estranho é parcialmente correto: se isso aconteceu para terminar, é certo que x deve ter contido (por acaso) o valor de um 's raiz quadrada. Em todos os outros casos, ele não será encerrado; portanto, não é totalmente correto.
Enquanto regra para correção total
Se a regra while ordinária acima for substituída pela seguinte, o cálculo de Hoare também pode ser usado para provar a correção total , ou seja, a terminação, bem como a correção parcial. Normalmente, colchetes são usados aqui em vez de colchetes para indicar a noção diferente de correção do programa.
Nessa regra, além de manter a invariante do laço, também se prova a terminação por meio de uma expressão t , chamada de variante do laço , cujo valor diminui estritamente em relação a uma relação bem fundada < em algum conjunto de domínio D durante cada iteração. Uma vez que < é bem fundamentado, uma cadeia estritamente decrescente de membros de D pode ter apenas comprimento finito, então t não pode continuar diminuindo para sempre. (Por exemplo, a ordem usual < é bem fundamentada em números inteiros positivos , mas nem em números inteiros nem em números reais positivos ; todos esses conjuntos são significados na matemática, não no sentido de computação, eles são todos infinitos em particular.)
Dado o invariante de laço P , a condição B deve implicar que t não é um elemento mínimo de D , caso contrário o corpo S não poderia diminuir mais t , isto é, a premissa da regra seria falsa. (Esta é uma das várias notações para correção total.)
Retomando o primeiro exemplo da seção anterior , para uma prova de correção total de
a regra while para correção total pode ser aplicada com, por exemplo, D sendo os inteiros não negativos com a ordem usual, e a expressão t sendo , que então, por sua vez, requer provar
Falando informalmente, temos que provar que a distância diminui a cada ciclo do loop, embora sempre permaneça não negativa; esse processo pode prosseguir apenas por um número finito de ciclos.
O objetivo de prova anterior pode ser simplificado para
- ,
que pode ser comprovado da seguinte forma:
- é obtido pela regra de atribuição, e
- pode ser fortalecido pela regra de conseqüência.
Para o segundo exemplo da seção anterior , é claro que nenhuma expressão t pode ser encontrada diminuída pelo corpo do loop vazio, portanto, o término não pode ser provado.
Veja também
- Asserção (computação)
- Comunicação de processos sequenciais
- Projeto por contrato
- Semântica denotacional
- Lógica dinâmica
- Edsger W. Dijkstra
- Loop invariante
- Semântica de transformador de predicado
- Verificação do programa
- Cálculo de refinamento
- Lógica de separação
- Cálculo sequencial
- Análise de código estático
Notas
Referências
Leitura adicional
- Robert D. Tennent. Especificação de software (um livro que inclui uma introdução à lógica Hoare, escrita em 2002) ISBN 0-521-00401-2
links externos
- KeY-Hoare é um sistema de verificação semiautomático construído com base no provador do teorema KeY . Possui um cálculo Hoare para uma linguagem enquanto simples.
- j-Algo-modul Hoare calculus - Uma visualização do cálculo Hoare no programa de visualização de algoritmo j-Algo