Lógica de Hoare

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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 subsequêncialmente aprimrada por Hoare e outros pesquisadores.[1] A idéia original havia sido idealizada pelo trabalho de Robert Floyd, que publicou um sistema similar[2] para fluxogramas.

Tripla de Hoare[editar | editar código-fonte]

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

\{P\}\;C\;\{Q\}

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[editar | editar código-fonte]

A lógica de Hoare padrão proporciona apenas corretude parcial, o encerramento do laço precisa ser provada 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", então 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[editar | editar código-fonte]

Axioma de Declaração Vazia[editar | editar código-fonte]

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.

 \frac{}{\{P\}\ \textbf{skip}\ \{P\}} \!

Axioma da Atribuição[editar | editar código-fonte]

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:

 \frac{}{\{P[E/x]\}\ x:=E \ \{P\} } \!

Aqui P[E/x] denota a expressão P em todas as ocorrências livres da variável x foram substituídas pela expressão E.

O axioma da atribuição indica que a validade de \{P[E/x]\} é equivalente à validade na atribuição posterior de \{P\}. Portanto se \{P[E/x]\} era verdade antes da atribuição, pelo axioma da atribuição, então \{P\} seria verdade subsequente a isso. Reciprocamente, se \{P[E/x]\} era falso antes da afirmação de artribuição, \{P\} deve ser falso consequentemente.

Isso é equivalente a dizer que para encontrar a pré-condição, primeiro tomamos a pós-condição e substituimos todas as ocorrências no lado esquerdo da datribuição com o lado direito. Cuidado para não tentar executar isso de "trás-para-frente" seguindo a maneira incorreta de pensar: \{P\} V :=E \{P[V/E]\}

Exemplos com triplas válidas incluem:

  • \{x+1 = 43\}\ y:=x + 1\ \{ y = 43 \}\!
  • \{x + 1 \leq N \}\ x := x  + 1\ \{x \leq N\}\ \!

O axioma da atribuição porposto por Hoare não se aplica quando mais de um nome pode se referir ao mesmo valor tomado. Por exemplo,

\{ A \} \ x := 2\ \{y = 3 \}

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 é atribuido como 2.

Regra da Composição[editar | editar código-fonte]

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):

 \frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \!

Por exemplo, considerando as duas instâncias seguintes do axioma da atribuição:

\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}

e

\{ y = 43\} \ z:=y\ \{z =43 \}

Pela regra sequencial, podemos concluir:

\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}

Regra Condicional[editar | editar código-fonte]

\frac { \{B \wedge P\}\ S\ \{Q\}\ ,\ \{\neg B \wedge P \}\ T\ \{Q\} }
              { \{P\}\ \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif}\ \{Q\} } \!

Regra da Consequência[editar | editar código-fonte]


\frac {  P^\prime \rightarrow\ P\ ,\ \lbrace P \rbrace\ S\ \lbrace Q \rbrace\ ,\ Q \rightarrow\ Q^\prime }
 	{ \lbrace P^\prime\ \rbrace\ S\ \lbrace Q^\prime\rbrace }
\!

Regra do Laço[editar | editar código-fonte]

\frac { \{P \wedge B \}\ S\ \{P\} }
              { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} }
\!

Aqui P é a invariável de laço.

regra do Laço para Corretude Total[editar | editar código-fonte]


\frac { <\;\textrm{is\ well-founded,}\;[P \wedge B \wedge t = z ]\ S\ [P \wedge t < z ]}
              { [P]\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ [\neg B \wedge P] }
\!

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 by membros decrescentes ode uma sequência finita. Também pode-se notar que colchetes são usados aqui em lugar de chaves para denotar corretude total, i.e. encerramento bom como corretude parcial. (essa é uma das várias notações para corretude total)

Exemplos[editar | editar código-fonte]

Example 1
\{x+1 = 43\}\! \ y:=x + 1\ \! \{ y = 43 \}\! (Axioma da Atribuição)
( x + 1 = 43 \Leftrightarrow x = 42 )
\{x=42\}\! \ y:=x + 1\ \! \{y=43 \land x=42\}\! (Regra da Consequência)
Example 2
\{x + 1 \leq N \}\! \ x := x  + 1\ \! \{x \leq N\}\ \! (Axioma da Atribuição)
( x < N \implies x + 1 \leq N para x, N tipos inteiros)
\{x < N \}\! \ x := x  + 1\ \! \{x \leq N\}\ \! (Regra da Consequência)

Referências

  1. C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–580,583 October 1969. doi:10.1145/363235.363259
  2. R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.

Ver também[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]

  • 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