Lógica de Hoare (também conhecida como lógica de Floyd–Hoare ou regras de Hoare) é um sistema formal com um conjunto de regras lógicas para um raciocínio rigoroso sobre a corretude na computação. Proposta em 1969 pelo cientista da computação e lógico britânico C. A. R. Hoare; e subsequencialmente aprimorada por Hoare e outros pesquisadores.C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–580,583 October 1969. A ideia original havia sido idealizada pelo trabalho de Robert Floyd, que publicou um sistema similarR. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967. para fluxogramas.
Tripla de Hoare O aspecto principal da lógica de Hoare é a Tripla de Hoare. A tripla descreve como a execução de uma parte do código muda o estado da computação. A tripla de Hoare é expressa na forma
onde P e Q são asserções e C é um comando. P é chamado de pré-condição e Q de pós-condição: quando a pré-condição é conhecida, o comando estabelece a pós-condição. Asserções são fórmulas na lógica de predicados.
A lógica de Hoare fornece axiomas e regras de inferência para todas as construções de uma simples linguagem de programação imperativa. Além disso, nas regras para a linguagem simples, das anotações originais de Hoare, regras para construção de outras linguagens foram desenvolvidas desde então, por Hoare e alguns outros pesquisadores. Há regras para concorrência, sub-rotina, salto e ponteiros.
Corretude parcial e total
A lógica de Hoare padrão proporciona apenas corretude parcial; o encerramento do laço precisa ser provado separadamente. Portanto, a leitura intuitiva da tripla de Hoare é: Sempre que P detém o estado antes da execução de C, então Q deterá posteriormente; ou C não encerra. Note que se C não encerra, então não há "posteriormente"; logo, Q pode ser, sem dúvidas, afirmação. Realmente, podemos escolher Q como falso para expressar que C não encerra.
Corretude total também pode ser provada pela versão estendida da Regra do Laço.
Regras Axioma de declaração vazia
A regra da declaração vazia estabelece que a afirmação skip não muda o estado do programa; portanto, o que detinha verdade antes de skip também deterá verdade após esta afirmação.
Axioma da atribuição
O axioma da atribuição institui que depois da atribuição, qualquer predicado se mantém para a variável que era originalmente verdade no lado direito da atribuição:
Aqui, denota a expressão P em todas as ocorrências livres da variável x que foram substituídas pela expressão E.
O axioma da atribuição indica que a validade de é equivalente à validade na atribuição posterior de . Portanto, se era verdade antes da atribuição, pelo axioma da atribuição, então seria verdade subsequente a isso. Reciprocamente, se era falso antes da afirmação de atribuição, deve ser falso consequentemente.
Isso é equivalente a dizer que para encontrar a pré-condição, primeiro tomamos a pós-condição e substituímos todas as ocorrências no lado esquerdo da atribuição com o lado direito. Cuidado para não tentar executar isso de "trás-para-frente", seguindo a maneira incorreta de pensar:
Exemplos com triplas válidas incluem:
O axioma da atribuição proposto por Hoare não se aplica quando mais de um nome pode se referir ao mesmo valor tomado. Por exemplo,
não é uma afirmação verdadeira se x e y referem-se a mesma variável, porque nenhuma pré-condição A pode implicar y ser 3 depois que x é atribuído como 2.
Regra da composição
A regra da composição de Hoare se aplica a programas S e T executados sequencialmente, onde S é executado anteriormente a T; e é escrito S;T (onde P é a pré-condição, R é a pós-condição e Q a condição intermediária):
Por exemplo, considerando as duas instâncias seguintes do axioma da atribuição:
e
Pela regra sequencial, podemos concluir:
Regra condicional
Regra da consequência
Regra do laço
Aqui P é a "invariável de laço".
Regra do laço para corretude total
Nesta regra, além de manter a invariável de laço, também fornecemos encerramento pela forma do termo, chamado variável de laço, aqui t, cujo valor decai estritamente com respeito à relação bem-fundada durante cada iteração. Note que, dado invariável P, a condição B deve implicar que t não é elemento minimal do seu escopo; caso contrário, a premissa desta regra seria falsa. Porque a relação "<" é bem-formada, cada passo do laço é contado por membros decrescentes de uma sequência finita. Também pode-se notar que colchetes são usados aqui, em lugar de chaves, para denotar corretude total. Ou seja, pode-se definir encerramento bom como corretude parcial (essa é uma das várias notações para corretude total).
Exemplos
{|style="text-align:left" | style="background:silver;" colspan="4"|Exemplo 1
|(Axioma da atribuição)
|(Regra da consequência) |- | style="background:silver;" colspan="4"|Exemplo 2
|(Axioma da atribuição)
|( para x, N tipos inteiros)
|(Regra da consequência)
Ver também CSP (matemática) Programação por contrato Semântica denotacional Dynamic logic Edsger Dijkstra Verificação formal
Ligações externas Project Bali has defined Hoare logic-style rules for a subset of the Java programming language, for use with the Isabelle theorem prover KeY-Hoare is a semi-automatic verification system built on top of the KeY theorem prover. It features a Hoare calculus for a simple while language. j-Algo-modul Hoare calculus — A visualisation of the Hoare calculus in the algorithm visualisation program j-Algo
Categoria:Ciência da computação