Lógica de Hoare

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.^[1] A idéia original havia sido idealizada pelo trabalho de Robert Floyd, que publicou um sistema similar^[2] 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

${\displaystyle \{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

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.

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

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:

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

Aqui, ${\displaystyle P[E/x]}$ 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 ${\displaystyle \{P[E/x]\}}$ é equivalente à validade na atribuição posterior de ${\displaystyle \{P\}}$. Portanto, se ${\displaystyle \{P[E/x]\}}$ era verdade antes da atribuição, pelo axioma da atribuição, então ${\displaystyle \{P\}}$ seria verdade subsequente a isso. Reciprocamente, se ${\displaystyle \{P[E/x]\}}$ era falso antes da afirmação de atribuição, ${\displaystyle \{P\}}$ 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: ${\displaystyle \{P\}V:=E\{P[V/E]\}}$

Exemplos com triplas válidas incluem:

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

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,

${\displaystyle \{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 é 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):

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

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

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

e

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

Pela regra sequencial, podemos concluir:

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

Regra condicional

${\displaystyle {\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

${\displaystyle {\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

${\displaystyle {\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

${\displaystyle {\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 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

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

Referências

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