Semântica do transformador de predicado - Predicate transformer semantics

Semântica
Lingüística Lógico
Subcampos Computacional Lexical ( léxico , lexicologia ) Estatístico Estrutural Tópicos Análise Composicionalidade Contexto (uso da linguagem) Teoria do protótipo Dinâmica de força Problemas de linguística não resolvidos Teoria das Descrições
Informática
Tipos Açao Algébrico Axiomático Categórico Simultaneidade Denotacional Jogo Operacional Predicado transformacional Teoria Interpretação abstrata Gráfico semântico abstrato Correspondência semântica Análise Latente Aprendizado de máquina Formulários Sistema de arquivo semântico Web Semântica Wiki semântico
Língua Linguística
v t e

A semântica do transformador de predicado foi introduzida por Edsger Dijkstra em seu artigo seminal " Comandos protegidos, não-determinação e derivação formal de programas ". Eles definem a semântica de um paradigma de programação imperativo , atribuindo a cada instrução nesta linguagem um transformador de predicado correspondente : uma função total entre dois predicados no espaço de estado da instrução. Nesse sentido, a semântica do transformador de predicado é uma espécie de semântica denotacional . Na verdade, em comandos protegidos , Dijkstra usa apenas um tipo de transformador de predicado: as pré - condições mais fracas conhecidas (veja abaixo).

Além disso, a semântica do transformador de predicado é uma reformulação da lógica de Floyd-Hoare . Enquanto a lógica de Hoare é apresentada como um sistema dedutivo , a semântica do transformador de predicado (seja pelas pré-condições mais fracas ou pelas pós-condições mais fortes, veja abaixo) são estratégias completas para construir deduções válidas da lógica de Hoare. Em outras palavras, eles fornecem um algoritmo eficaz para reduzir o problema de verificar um triplo de Hoare ao problema de provar uma fórmula de primeira ordem . Tecnicamente, a semântica do transformador de predicado executa um tipo de execução simbólica de declarações em predicados: a execução é executada para trás no caso das pré-condições mais fracas ou para frente no caso das pós-condições mais fortes.

Condições prévias mais fracas

Definição

Para uma declaração S e uma pós - condição R , uma pré - condição mais fraca é um predicado Q tal que para qualquer pré-condição , se e somente se . Em outras palavras, é o "mais frouxo" ou menos exigência restritiva necessária para garantia de que R mantém após S . Singularidade segue facilmente a partir da definição: Se ambos Q e Q' são mais fracas condições prévias, em seguida, pela definição de modo e assim , e assim . Denote pela pré-condição mais fraca para a declaração S e pós-condição R . ${\ displaystyle P}$${\ displaystyle \ {P \} S \ {R \}}$${\ displaystyle P \ Rightarrow Q}$${\ displaystyle \ {Q '\} S \ {R \}}$${\ displaystyle Q '\ Rightarrow Q}$${\ displaystyle \ {Q \} S \ {R \}}$${\ displaystyle Q \ Rightarrow Q '}$${\ displaystyle Q = Q '}$${\ displaystyle wp (S, R)}$

Pular

${\ displaystyle wp ({\ textbf {ignorar}}, R) \ = \ R}$

Abortar

${\ displaystyle wp ({\ textbf {abortar}}, R) \ = \ {\ textbf {false}}}$

Atribuição

Damos a seguir duas precondições mais fracas equivalentes para a instrução de atribuição. Nestas fórmulas, é uma cópia de R onde ocorrências livres de x são substituídos por E . Portanto, aqui, a expressão E é implicitamente coagida em um termo válido da lógica subjacente: é, portanto, uma expressão pura , totalmente definida, encerrando e sem efeito colateral. ${\ displaystyle R [x \ leftarrow E]}$

• versão 1:

${\ displaystyle wp (x: = E, R) \ = \ \ forall y, y = E \ Rightarrow R [x \ leftarrow y]}$ onde y é uma variável nova (representando o valor final da variável x )

• versão 2:

${\ displaystyle wp (x: = E, R) \ = \ R [x \ leftarrow E]}$

A primeira versão evita uma duplicação potencial de x em R , ao passo que a segunda versão é mais simples quando há, no máximo, uma única ocorrência de x em R . A primeira versão também revela uma profunda dualidade entre a pré-condição mais fraca e a pós-condição mais forte (veja abaixo).

Um exemplo de cálculo válido de wp (usando a versão 2) para atribuições com variável de valor inteiro x é:

${\ displaystyle {\ begin {array} {rcl} wp (x: = x-5, x> 10) & = & x-5> 10 \\ & \ Leftrightarrow & x> 15 \ end {array}}}$

Isso significa que para que a pós-condição x> 10 seja verdadeira após a atribuição, a pré-condição x> 15 deve ser verdadeira antes da atribuição. Esta também é a "pré-condição mais fraca", pois é a restrição "mais fraca" no valor de x que torna x> 10 verdadeiro após a atribuição.

Seqüência

${\ displaystyle wp (S_ {1}; S_ {2}, R) \ = \ wp (S_ {1}, wp (S_ {2}, R))}$

Por exemplo,

${\ displaystyle {\ begin {array} {rcl} wp (x: = x-5; x: = x * 2 \, \ x> 20) & = & wp (x: = x-5, wp (x: = x * 2, x> 20)) \\ & = & wp (x: = x-5, x * 2> 20) \\ & = & (x-5) * 2> 20 \\ & = & x> 15 \ fim {array}}}$

Condicional

${\ displaystyle wp ({\ textbf {if}} \ E \ {\ textbf {then}} \ S_ {1} \ {\ textbf {else}} \ S_ {2} \ {\ textbf {end}}, R ) \ = \ (E \ Rightarrow wp (S_ {1}, R)) \ wedge (\ neg E \ Rightarrow wp (S_ {2}, R))}$

Por exemplo:

${\ displaystyle {\ begin {array} {rcl} wp ({\ textbf {if}} \ x <y \ {\ textbf {then}} \ x: = y \ {\ textbf {else}} \; \; {\ textbf {skip}} \; \; {\ textbf {end}}, \ x \ geq y) & = & (x <y \ Rightarrow wp (x: = y, x \ geq y)) \ \ wedge \ (\ neg (x <y) \ Rightarrow wp ({\ textbf {pular}}, x \ geq y)) \\ & = & (x <y \ Rightarrow y \ geq y) \ \ wedge \ (\ neg (x <y) \ Rightarrow x \ geq y) \\ & \ Leftrightarrow & {\ textbf {true}} \ end {array}}}$

Loop while

Correção Parcial

Ignorando a terminação por um momento, podemos definir a regra para a pré-condição liberal mais fraca , denotada wlp , usando um predicado I , chamado de invariante de loop , normalmente fornecido pelo programador:

${\ displaystyle wlp ({\ textbf {while}} \ E \ {\ textbf {do}} \ S \ {\ textbf {done}}, R) \ = \ {\ begin {array} {l} I \\ \ wedge \ \ forall y, ((E \ wedge I) \ Rightarrow wlp (S, I)) [x \ leftarrow y] \\\ wedge \ \ forall y, ((\ neg E \ wedge I) \ Rightarrow R ) [x \ leftarrow y] \ end {array}}}$

Isso simplesmente afirma que (1) o invariante deve ser mantido no início do loop; (2) adicionalmente, para qualquer estado inicial y , o invariante e o guarda tomados juntos são fortes o suficiente para estabelecer a pré-condição mais fraca necessária para que o corpo do laço seja capaz de restabelecer o invariante; (3) finalmente, se e quando o loop termina em um determinado estado y , o fato de o protetor de loop ser falso junto com a invariante deve ser capaz de estabelecer a pós-condição necessária.

Correção Total

Para mostrar correção total, também temos que mostrar que o loop termina. Para isso, definimos uma relação bem fundamentada no espaço de estados denotada "<" e chamada de variante de loop . Portanto, temos:

${\ displaystyle wp ({\ textbf {while}} \ E \ {\ textbf {do}} \ S \ {\ textbf {done}}, R) \ = \ {\ begin {array} {l} I \\ \ wedge \ \ forall y, ((E \ wedge I) \ Rightarrow wp (S, I \ wedge x <y)) [x \ leftarrow y] \\\ wedge \ \ forall y, ((\ neg E \ wedge I) \ Rightarrow R) [x \ leftarrow y] \ end {array}}}$ onde y é uma nova tupla de variáveis

Informalmente, na conjunção acima de três fórmulas:

• o primeiro significa aquele invariante que devo inicialmente manter;
• o segundo significa que o corpo do loop (por exemplo, instrução S ) deve preservar o invariante e diminuir a variante: aqui, a variável y representa o estado inicial da execução do corpo;
• o último significa que R deve ser estabelecido no final do loop: aqui, a variável y representa o estado final do loop.

Na semântica dos transformadores de predicado, invariante e variante são construídos imitando o teorema de ponto fixo de Kleene . Abaixo, esta construção é esboçada na teoria dos conjuntos . Assumimos que U é um conjunto que denota o espaço de estados. Primeiro, definimos uma família de subconjuntos de U denotados por indução sobre o número natural k . Informalmente representa o conjunto de estados iniciais que tornam R satisfeito após menos de k iterações do loop: ${\ displaystyle (A_ {k}) _ {k \ in \ mathbb {N}}}$ ${\ displaystyle A_ {k}}$

${\ displaystyle {\ begin {array} {rcl} A_ {0} & = & \ emptyset \\ A_ {k + 1} & = & \ left \ {\ y \ in U \ | \ ((E \ Rightarrow wp (S, x \ in A_ {k})) \ wedge (\ neg E \ Rightarrow R)) [x \ leftarrow y] \ \ right \} \\\ end {array}}}$

Então, definimos:

• invariante I como o predicado .${\ displaystyle \ existe k, x \ in A_ {k}}$
• variante como a proposição${\ displaystyle y <z}$${\ displaystyle \ exists i, y \ in A_ {i} \ wedge (\ forall j, z \ in A_ {j} \ Rightarrow i <j)}$

Com essas definições, reduz-se à fórmula . ${\ displaystyle wp ({\ textbf {while}} \ E \ {\ textbf {do}} \ S \ {\ textbf {done}}, R)}$${\ displaystyle \ existe k, x \ in A_ {k}}$

No entanto, na prática, tal construção abstrata não pode ser tratada de forma eficiente por provadores de teoremas. Conseqüentemente, invariantes e variantes de loop são fornecidos por usuários humanos ou inferidos por algum procedimento de interpretação abstrato .

Comandos protegidos não determinísticos

Na verdade, a Guarded Command Language (GCL) de Dijkstra é uma extensão da linguagem imperativa simples fornecida até aqui com declarações não determinísticas. Na verdade, GCL pretende ser uma notação formal para definir algoritmos. Declarações não determinísticas representam escolhas deixadas para a implementação real (em uma linguagem de programação eficaz): propriedades provadas em declarações não determinísticas são garantidas para todas as escolhas possíveis de implementação. Em outras palavras, as pré-condições mais fracas de declarações não determinísticas garantem

• que existe uma execução final (por exemplo, existe uma implementação),
• e, que o estado final de toda execução de término satisfaz a pós-condição.

Observe que as definições da pré-condição mais fraca fornecidas acima (em particular para o loop while ) preservam essa propriedade.

Seleção

A seleção é uma generalização da instrução if :

${\ displaystyle wp (\ mathbf {if} \ E_ {1} \ rightarrow S_ {1} \ [\!] \ \ ldots \ [\!] \ E_ {n} \ rightarrow S_ {n} \ \ mathbf {fi }, R) \ = {\ begin {array} {l} (E_ {1} \ vee \ ldots \ vee E_ {n}) \\\ wedge \ (E_ {1} \ Rightarrow wp (S_ {1}, R)) \\\ ldots \\\ wedge \ (E_ {n} \ Rightarrow wp (S_ {n}, R)) \\\ end {array}}}$

Aqui, quando dois guardas e são simultaneamente verdadeiros, a execução desta instrução pode executar qualquer uma das instruções associadas ou . ${\ displaystyle E_ {i}}$${\ displaystyle E_ {j}}$${\ displaystyle S_ {i}}$${\ displaystyle S_ {j}}$

Repetição

A repetição é uma generalização da instrução while de maneira semelhante.

Declaração de especificação (ou pré-condição mais fraca de chamada de procedimento)

O cálculo de refinamento estende declarações não determinísticas com a noção de declaração de especificação . Informalmente, esta instrução representa uma chamada de procedimento em caixa preta, onde o corpo do procedimento não é conhecido. Normalmente, usando uma sintaxe próxima ao Método B , uma instrução de especificação é escrita

${\ displaystyle P \ |}$ @${\ displaystyle y. \ Q \ rightarrow x: = y}$

Onde

• x é a variável global modificada pela declaração,
• P é um predicado que representa a pré-condição,
• y é uma nova variável lógica, limitada em Q , que representa o novo valor de x não deterministicamente escolhido pela declaração,
• Q é um predicado que representa uma pós-condição, ou mais exatamente um guarda: em Q , a variável x representa o estado inicial ey denota o estado final.

A pré-condição mais fraca da declaração de especificação é dada por:

${\ displaystyle wp (P \ |}$ @${\ displaystyle y. \ Q \ rightarrow x: = y \, \ R) \ = \ P \ wedge \ forall z, Q [y \ leftarrow z] \ Rightarrow R [x \ leftarrow z]}$ onde z é um novo nome

Além disso, uma declaração S implementa tal declaração de especificação se e somente se o seguinte predicado for uma tautologia:

${\ displaystyle \ forall x_ {0}, (P \ Rightarrow wp (S, Q [x \ leftarrow x_ {0}] [y \ leftarrow x])) [x \ leftarrow x_ {0}]}$ onde é um novo nome (denotando o estado inicial) ${\ displaystyle x_ {0}}$

De fato, em tal caso, a seguinte propriedade é assegurada para toda a pós-condição R (esta é uma consequência direta da monotonicidade wp , veja abaixo):

${\ displaystyle wp (P \ |}$ @${\ displaystyle y. \ Q \ rightarrow x: = y \, \ R) \ Rightarrow wp (S, R)}$

Informalmente, esta última propriedade garante que qualquer prova sobre alguma declaração envolvendo uma especificação permaneça válida ao substituir esta especificação por qualquer uma de suas implementações.

Outros transformadores de predicado

Pré-condição liberal mais fraca

Uma variante importante da condição prévia mais fraco é o mais fraco condição prévia liberal , que origina o estado mais fraco em que S seja não terminar ou estabelece R . Portanto, difere do wp por não garantir o encerramento. Conseqüentemente, corresponde à lógica de Hoare em correção parcial: para a linguagem de instrução fornecida acima, wlp difere de wp apenas no laço while , por não exigir uma variante (veja acima). ${\ displaystyle wlp (S, R)}$

Pós-condição mais forte

Dada S uma declaração e R uma pré - condição (um predicado no estado inicial), então é sua pós-condição mais forte : ela implica qualquer pós-condição satisfeita pelo estado final de qualquer execução de S, para qualquer estado inicial que satisfaça R. Em outras palavras, um triplo de Hoare pode ser demonstrado na lógica de Hoare se e somente se o predicado abaixo for válido: ${\ displaystyle sp (S, R)}$${\ displaystyle \ {P \} S \ {Q \}}$

${\ displaystyle \ forall x, sp (S, P) \ Rightarrow Q}$

Normalmente, as pós-condições mais fortes são usadas na correção parcial. Portanto, temos a seguinte relação entre as pré-condições liberais mais fracas e as pós-condições mais fortes:

${\ displaystyle (\ forall x, P \ Rightarrow wlp (S, Q)) \ \ Leftrightarrow \ (\ forall x, sp (S, P) \ Rightarrow Q)}$

Por exemplo, na atribuição, temos:

${\ displaystyle sp (x: = E, R) \ = \ \ existe y, x = E [x \ leftarrow y] \ wedge R [x \ leftarrow y]}$ onde y é fresco

Acima, a variável lógica y representa o valor inicial da variável x . Portanto,

${\ displaystyle sp (x: = x-5, x> 15) \ = \ \ existe y, x = y-5 \ wedge y> 15 \ \ Leftrightarrow \ x> 10}$

Na sequência, parece que sp corre para a frente (enquanto wp corre para trás):

${\ displaystyle sp (S_ {1}; S_ {2} \, \ R) \ = \ sp (S_ {2}, sp (S_ {1}, R))}$

Transformadores de predicado de vitória e pecado

Leslie Lamport sugeriu vitória e pecado como transformadores de predicado para programação simultânea .

Propriedades de transformadores de predicado

Esta seção apresenta algumas propriedades características dos transformadores de predicado. Abaixo, T denota um transformador de predicado (uma função entre dois predicados no espaço de estados) e P um predicado. Por exemplo, T (P) pode denotar wp (S, P) ou sp (S, P) . Mantemos x como a variável do espaço de estados.

Monotônico

Os transformadores predicados de interesse ( wp , wlp e sp ) são monotônicos . Um transformador de predicado T é monotônico se e somente se:

${\ displaystyle (\ forall x, P \ Rightarrow Q) \ Rightarrow (\ forall x, T (P) \ Rightarrow T (Q))}$

Esta propriedade está relacionada à regra de conseqüência da lógica de Hoare .

Rigoroso

Um transformador de predicado T é estrito iff:

${\ displaystyle T (\ mathbf {false}) \ \ Leftrightarrow \ \ mathbf {false}}$

Por exemplo, wp é estrito, enquanto wlp geralmente não é. Em particular, se a instrução S não pode terminar, então é satisfatória. Nós temos ${\ displaystyle wlp (S, \ mathbf {false})}$

${\ displaystyle wlp (\ mathbf {while} \ \ mathbf {true} \ \ mathbf {do} \ \ mathbf {skip} \ \ mathbf {done}, \ mathbf {false}) \ \ Leftrightarrow \ mathbf {true}}$

Na verdade, true é um invariante válido desse loop.

Terminando

Um transformador de predicado T está encerrando iff:

${\ displaystyle T (\ mathbf {true}) \ \ Leftrightarrow \ \ mathbf {true}}$

Na verdade, esta terminologia faz sentido apenas para rigorosas transformadores predicado: de facto, é a mais fraca condição prévia garantindo-terminação de S . ${\ displaystyle wp (S, \ mathbf {true})}$

Parece que nomear esta propriedade de não aborto seria mais apropriado: em correção total, não rescisão é aborto, enquanto em correção parcial, não é.

Conjuntivo

Um transformador de predicado T é conjuntivo iff:

${\ displaystyle T (P \ wedge Q) \ \ Leftrightarrow \ (T (P) \ wedge T (Q))}$

Este é o caso de , mesmo se a afirmação S não for determinística como uma instrução de seleção ou uma instrução de especificação. ${\ displaystyle wp (S ,.)}$

Disjuntivo

Um transformador de predicado T é disjuntivo se:

${\ displaystyle T (P \ vee Q) \ \ Leftrightarrow \ (T (P) \ vee T (Q))}$

Geralmente, esse não é o caso quando S é não determinístico. De fato, considere uma afirmação não determinística S escolhendo um booleano arbitrário. Esta declaração é dada aqui como a seguinte declaração de seleção : ${\ displaystyle wp (S ,.)}$

${\ displaystyle S \ = \ \ mathbf {if} \ \ mathbf {true} \ rightarrow x: = 0 \ [\!] \ \ mathbf {true} \ rightarrow x: = 1 \ \ mathbf {fi}}$

Então, reduz-se à fórmula . ${\ displaystyle wp (S, R)}$${\ displaystyle R [x \ leftarrow 0] \ wedge R [x \ leftarrow 1]}$

Conseqüentemente, reduz-se à tautologia${\ displaystyle wp (S, \ x = 0 \ vee x = 1)}$ ${\ displaystyle (0 = 0 \ vee 0 = 1) \ wedge (1 = 0 \ vee 1 = 1)}$

Considerando que, a fórmula se reduz à proposição errada . ${\ displaystyle wp (S, x = 0) \ vee wp (S, x = 1)}$ ${\ displaystyle (0 = 0 \ wedge 1 = 0) \ vee (1 = 0 \ wedge 1 = 1)}$

O mesmo contra-exemplo pode ser reproduzido usando uma declaração de especificação (veja acima) em vez disso:

${\ displaystyle S \ = \ \ mathbf {true} \ |}$ @${\ displaystyle y. \ y \ in \ {0,1 \} \ rightarrow x: = y}$

Formulários

• Os cálculos das pré-condições mais fracas são amplamente usados ​​para verificar estaticamente as asserções em programas usando um provador de teoremas (como solucionadores de SMT ou assistentes de prova ): consulte Frama-C ou ESC / Java2 .
• Ao contrário de muitos outros formalismos semânticos, a semântica do transformador de predicado não foi projetada como uma investigação dos fundamentos da computação. Em vez disso, a intenção era fornecer aos programadores uma metodologia para desenvolver seus programas como "corretos por construção" em um "estilo de cálculo". Esse estilo "de cima para baixo" foi defendido por Dijkstra e N. Wirth . Foi formalizado posteriormente por R.-J. Voltar e outros no cálculo de refinamento . Algumas ferramentas como o Método B agora fornecem raciocínio automatizado para promover essa metodologia.
• Na metateoria da lógica de Hoare , as pré-condições mais fracas aparecem como uma noção-chave na prova de completude relativa .

Além dos transformadores de predicado

Pré-condições mais fracas e pós-condições mais fortes de expressões imperativas

Na semântica dos transformadores de predicado, as expressões são restritas aos termos da lógica (veja acima). No entanto, essa restrição parece muito forte para a maioria das linguagens de programação existentes, onde as expressões podem ter efeitos colaterais (chamada para uma função que tem um efeito colateral), não podem terminar ou abortar (como a divisão por zero ). Existem muitas propostas para estender as pré-condições mais fracas ou as pós-condições mais fortes para as linguagens de expressão imperativas e, em particular, para as mônadas .

Entre eles, a Teoria dos Tipos de Hoare combina a lógica de Hoare para uma linguagem semelhante a Haskell , lógica de separação e teoria dos tipos . Este sistema está atualmente implementado como uma biblioteca Coq chamada Ynot . Nessa linguagem, a avaliação de expressões corresponde a cálculos de pós-condições mais fortes .

Transformadores de predicado probabilístico

Transformadores de predicado probabilísticos são uma extensão dos transformadores de predicado para programas probabilísticos . Na verdade, tais programas têm muitas aplicações em criptografia (ocultação de informações usando algum ruído aleatório), sistemas distribuídos (quebra de simetria).

Veja também

• Semântica axiomática - inclui semântica de transformador de predicado
• Lógica dinâmica - onde os transformadores de predicado aparecem como modalidades
• Semântica formal de linguagens de programação - uma visão geral

Notas

Referências