Qual é a regra de atribuição do jeito que está na Lógica de Hoare?

Question

Qual é a regra de atribuição do jeito que está nos Hoare de Lógica/Semântica Axiomática?Eu não posso quebrar a minha cabeça em torno do qual a regra de atribuição é de trás para frente a partir do que eu esperava.

Eu entendo Hoare lógica é para provar formal de proposições, de o estado de um programa como os comandos são executados.Assim, se executar o comando $$x:=e$$ Eu teria esperado que o próximo estado tem de substituição...mas parece que a substituição acontece antes de nós executar a tarefa que eu acho bizarra.Eu teria esperado:

$$ \{ P \} x:= n \{P[e/x]\}$$

Dado que $P$ são declarações sobre o estado de programa.

Eu tenho certeza que existe uma boa explicação para isso, e desculpe se isso é uma questão básica, que eu sei que ele deve ser.Mas alguém pode explicar-me?

---

Pergunta Bônus:

Por que não podemos escrever a regra de atribuição como:

$$ \{ Q \} x:= n \{P[x/t]\}$$

observação NÃO é a mesma que a minha sugestão original, porque temos a $x$ e $e$ trocado em torno.i.e.no post condição sempre que temos uma $e$ colocamos um $x$ (o que é bom porque a declaração que acabou de executar é que $x$ contém o valor de $e$, então devemos ser capazes de substituir $e$ para $x$ no post condição, se a condição de ajuda.

---

Posts relacionados que eu li que não ajudaram:

• Hoare triplo para atribuição de P{x/B} x:=E {P}
• Taxas de lógica de Hoare
• https://www.quora.com/unanswered/Why-is-the-assignment-rule-the-way-it-is-in-Hoare-Logic
• https://www.reddit.com/r/ProgrammingLanguages/comments/e8suhh/why_is_the_assignment_rule_the_way_it_is_in_hoare/

---

Apêndice:

Para nos disléxicos, em esta pergunta é o que a substituição de notação significa:

$$ P[e/x] = P[e \x] $$

i.e.substitua cada ocorrência de $x$ com expressão/prazo/aí $e$.

Answer 1

Então, depois de ler e pensar mais sobre isso, esta é a minha explicação ( Obrigado software Fundações ):

A confusão chave para mim parece ser o significado de $ p [E / x] $ (substitui todas as instâncias gratuitas de x por e). O que isto faz é onde você vê o símbolo $ x $ Literalmente remova-o e coloque $ e $ . por exemplo. $ p [E / x]= (x + y + 1) [E / x] \ para p [E / x]= (E + Y + 1) $ Portanto, observe como $ x $ literalmente desapareceu da $ P $ . Então, o que queremos é uma vez que fazemos a tarefa:

$$ x:= e $$

que a declaração é verdadeira se tivéssemos $ x $ em vez de $ e $ . Então, se a regra é:

$$ \ {p [E / x] \} x:= e \ {p} $$

Então o que queremos é, quando conectar $ x $ para $ e $ Queremos o declaração em consideração ser verdadeira. Então, antes de começarmos o código, temos $ p [E / X] $ . Em seguida, nós executamos a tarefa e todas as instâncias da $ e $ desaparecem e recebemos $ x $ para substituí-los. Que deve ser verdadeiro se o código que correr fosse atribuído (já que $ x $ agora segure o valor $ E $ , para que você possa remover $ e $ '' s e lugar $ x $ ).

Isso é a explicação do conceito abstrato. Lets (descaradamente) use o exemplo dos fundações de software (SF):

.

{{y= 1}} x ::= y {{x= 1}} em inglês: Se começarmos em um estado em que o valor de Y é 1 e atribuímos y a x, então terminar em um estado em que X é 1. isto é, a propriedade de ser igual a 1 é transferida de y para x.

Outro parágrafo útil da SF:

.

Da mesma forma, em {{Y + z= 1}} x ::= y + z {{x= 1}} A mesma propriedade (sendo igual a um) é transferida para x da expressão y + z no lado direito da tarefa. Mais geralmente, se uma é qualquer expressão aritmética, então {{a= 1}} x ::= a {{x= 1}}} é um triplo de Hoare válido.

---

Adendo da grande observação do comentário:

.

É importante reconhecer que a regra { P. [ E. / X. ] } X. :=. E. { P. } permite tanto a expressão E. e a variável. X. para ocorrer na pós-condição. Em outras palavras, a regra de inferência permite que você deduza uma pós-condição em que qualquer subconjunto das ocorrências de E. Na pré-condição foram substituídos por X. , incluindo nenhum deles. Além disso, permite que você deduza todas essas diferentes pós-condições simultaneamente.

---

Responder ao bônus Por que é

1) $ \ {p [e / x] \} x:= e \ {p} $

melhor que

2) $ \ {\ \} x:= e \ {q [x / e] \} $ :

Além do ponto sutil da substituição de X por expressões que podem ser invisíveis (por exemplo, E= 0, devemos substituir $ 0 $ com um número infinito de $ x $ E se os zeros não estiverem lá ... As regras devem ser sintáticas, mas acho que é melhor evitar tais confusões), acho que esta é a razão: < / p >.

.

Qual a regra de atribuição deve capturar é que estamos atribuindo a expressão e à variável x. Assim, apenas x deve ser "substituído" por e. Intuitivamente, no código (ou mais precisamente o estado do programa $ \ sigma $ ) quando x começa a segurar o valor e, ele não significa aleatoriamente que em todos os lugares Pode haver um e torna-se x depois de executar a atribuição $ x:= e $ . De fato, o que significa é que agora nas condições postais temos X's. Agora esses X se não tivermos a tarefa, deveríamos ter o valor de $ e $ i.e. Nós somente "desfazer" a substituição / atribuição o comando de atribuição fez. Nem todas as outras expressão aleatória e. Em suma, a única maneira de saber onde colocar o e é iniciado no correio após a tarefa ter sido feita, então começando a partir daí. Se fizermos isso para trás, poderíamos estar substituindo e nós não queremos substituir (mesmo que eles fossem verdadeiros, que eu acho que eles devem desde que estamos dizendo que X detém o valor e depois de atribuir E para X).

Answer 2

Suponha que estamos executando o programa x := e, e deixe $\sigma$ ser o estado inicial, e $\sigma'$ ser o estado final.

O crucial intuição aqui está:o valor de $x$ no final estado $\sigma'$ é o mesmo que o valor da expressão $e$ no inicial estado $\sigma$.De fato, o último é o valor que atribuímos à $x$ com o comando x := e.

Por isso, se $P(-)$ é uma propriedade sobre os valores, a fórmula $P(\mbox{$x us$-em-o-final-estado})$ é equivalente a $P(\mbox{$e$-em-o-inicial-estado})$.Em outras palavras $P(x)$ no pós-condição (no estado $\sigma'$) é realmente equivalente a $P(e)$ no pré-condição (no estado $\sigma$).

Usando a substituição é apenas uma maneira mais formal de se considerar a pós-condição como uma "fórmula que depende $x$", i.é.como $P(x)$, e , em seguida, exigindo $P(e)$ como pré-requisito.