Linguagem de comando protegido - Guarded Command Language

A Guarded Command Language ( GCL ) é uma linguagem definida por Edsger Dijkstra para a semântica do transformador de predicado . Ele combina conceitos de programação de forma compacta, antes de o programa ser escrito em alguma linguagem de programação prática. Sua simplicidade facilita a comprovação da correção de programas, utilizando a lógica de Hoare .

Comando protegido

O comando protegido é o elemento mais importante da linguagem de comando protegido. Em um comando guardado, assim como o nome diz, o comando é "guardado". A guarda é uma proposição , que deve ser verdadeira antes que a instrução seja executada . No início da execução dessa declaração, pode-se supor que a guarda seja verdadeira. Além disso, se a guarda for falsa, a declaração não será executada. O uso de comandos protegidos torna mais fácil provar que o programa atende às especificações . A declaração costuma ser outro comando cauteloso.

Sintaxe

Um comando protegido é uma declaração da forma G → S, onde

  • G é uma proposição , chamada de guarda
  • S é uma declaração

Se G for verdadeiro, o comando protegido pode ser escrito simplesmente S.

Semântica

No momento em que G é encontrado em um cálculo, ele é avaliado.

  • Se G for verdadeiro, execute S
  • Se G for falso, olhe para o contexto para decidir o que fazer (em qualquer caso, não execute S)

Pular e Abortar

Ignorar e Abortar são declarações muito simples e importantes na linguagem de comandos protegidos. Abortar é a instrução indefinida: faça qualquer coisa. A instrução abort nem precisa terminar. É usado para descrever o programa ao formular uma prova, caso em que a prova geralmente falha. Skip é a instrução vazia: não faça nada. É usado no próprio programa, quando a sintaxe requer uma instrução, mas o programador não deseja que a máquina mude de estado .

Sintaxe

skip

abort

Semântica

  • Skip: não faça nada
  • Abortar: faça qualquer coisa

Atribuição

Atribui valores às variáveis .

Sintaxe

v := E

ou 

v0, v1, ..., vn := E0, E1, ..., En

Onde

  • v são variáveis ​​de programa
  • E são expressões do mesmo tipo de dados que suas variáveis ​​correspondentes

Concatenação

As instruções são separadas por um ponto e vírgula (;)

Seleção : se

A seleção (geralmente chamada de "instrução condicional" ou "instrução if") é uma lista de comandos protegidos, dos quais um é escolhido para execução. Se mais de um guarda for verdadeiro, uma instrução é escolhida de forma não determinística para ser executada. Se nenhum dos guardas for verdadeiro, o resultado é indefinido. Como pelo menos um dos guardas deve ser verdadeiro, a declaração vazia "pular" geralmente é necessária.

Sintaxe

if G0 → S0
| G1 → S1
...
| Gn → Sn
fi

Semântica

Após a execução de uma seleção, todos os protetores são avaliados. Se nenhum dos guardas for avaliado como verdadeiro, a execução da seleção é abortada, caso contrário, um dos guardas com o valor verdadeiro é escolhido de forma não determinística e a instrução correspondente é executada.

Exemplos

Simples

Em pseudocódigo : 

if a < b then
  set c to True
else
  set c to False

Em linguagem de comando protegida: 

if a < b → c := true
| a ≥ b → c := false
fi

Uso de pular

Em pseudocódigo: 

if error is True then 
  set x to 0

Em linguagem de comando protegida: 

if error = true → x := 0
| error = false → skip
fi

Se a segunda guarda for omitida e erro = False, o resultado será abortado.

Mais guardas verdadeiros

if a ≥ b → max := a
| b ≥ a → max := b
fi

Se a = b, a ou b é escolhido como o novo valor para o máximo, com resultados iguais. No entanto, alguém que está implementando isso pode descobrir que um é mais fácil ou mais rápido do que o outro. Como não há diferença para o programador, ele está livre para implementar de qualquer maneira.

Repetição : fazer

A repetição executa os comandos protegidos repetidamente até que nenhum dos guardas seja verdadeiro. Normalmente, há apenas um guarda.

Sintaxe

do G0 → S0
| G1 → S1
...
| Gn → Sn
od

Semântica

Após a execução de uma repetição, todos os guardas são avaliados. Se todos os guardas forem avaliados como falsos, o salto será executado. Caso contrário, um dos guardas com valor verdadeiro é escolhido de forma não determinística e a instrução correspondente é executada após a qual a repetição é executada novamente.

Exemplos

Algoritmo Euclidiano Original

a, b := A, B;
do a < b → b := b - a
 | b < a → a := a - b
od

Esta repetição termina quando a = b, caso em que a e b possuem o maior divisor comum de A e B.

Dijkstra vê neste algoritmo uma forma de sincronizar dois ciclos infinitos a := a - be de b := b - aforma que a≥0e b≥0permaneça verdadeiro.

Algoritmo Euclidiano estendido

a, b, x, y, u, v := A, B, 1, 0, 0, 1;
do b ≠ 0 →
   q, r := a div b, a mod b;
   a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v
od

Esta repetição termina quando b = 0, caso em que as variáveis ​​detêm a solução para a identidade de Bézout : xA + yB = mdc (A, B).

Classificação não determinística

do a>b → a, b := b, a
 | b>c → b, c := c, b
 | c>d → c, d := d, c
od

O programa continua permutando elementos enquanto um deles é maior que seu sucessor. Esta classificação de bolha não determinística não é mais eficiente do que sua versão determinística, mas mais fácil de provar: ela não irá parar enquanto os elementos não forem classificados e que a cada etapa ela classifique pelo menos 2 elementos.

Arg max

x, y = 1, 1 
do x≠n →
   if f(x) ≤ f(y) → x := x+1
    | f(x) ≥ f(y) → y := x; x := x+1
   fi
od

Este algoritmo encontra o valor 1 ≤ y ≤ n para o qual uma dada função inteira f é máxima. Não apenas o cálculo, mas também o estado final não é necessariamente determinado de forma única.

Formulários

Programas corretos por construção

Generalizar a congruência observacional dos Comandos Guardados em uma rede levou ao Cálculo de Refinamento . Isso foi mecanizado em Métodos Formais como o Método B, que permite derivar programas formalmente de suas especificações.

Circuitos assíncronos

Comandos protegidos são adequados para projetos de circuitos sem sensibilidade a atrasos porque a repetição permite atrasos relativos arbitrários para a seleção de diferentes comandos. Nesta aplicação, uma porta lógica conduzindo um nó y no circuito consiste em dois comandos protegidos, como segue: 

PullDownGuard → y := 0
PullUpGuard → y := 1

PullDownGuard e PullUpGuard são funções das entradas da porta lógica, que descrevem quando a porta puxa a saída para baixo ou para cima, respectivamente. Ao contrário dos modelos clássicos de avaliação de circuitos, a repetição de um conjunto de comandos protegidos (correspondendo a um circuito assíncrono) pode descrever com precisão todos os comportamentos dinâmicos possíveis desse circuito. Dependendo do modelo com o qual se deseja viver para os elementos do circuito elétrico, podem ser necessárias restrições adicionais aos comandos protegidos para que uma descrição de comandos protegidos seja inteiramente satisfatória. As restrições comuns incluem estabilidade, não interferência e ausência de comandos de auto-invalidação.

Verificação de modelo

Os comandos protegidos são usados ​​na linguagem de programação Promela , que é usada pelo verificador de modelo SPIN . O SPIN verifica a operação correta de aplicativos de software simultâneos.

De outros

O módulo Perl Commands :: Guarded implementa uma variante retificadora determinística nos comandos protegidos de Dijkstra.

Referências

  1. ^ Dijkstra, Edsger W . "EWD472: Comandos protegidos, não determinação e derivação formal de programas" (PDF) . Recuperado em 16 de agosto de 2006 .
  2. ^ Anne Kaldewaij (1990), Programming: The Derivation of Algorithms , Prentice Hall
  3. ^ Voltar, Ralph J (1978). "Sobre a correção das etapas de refinamento no desenvolvimento de programas (tese de doutorado)" (PDF) . Arquivado do original (pdf) em 20/07/2011.
  4. ^ Martin, Alain J. "Synthesis of Asynchronous VLSI Circuits" .