Lenguaje de comando protegido - Guarded Command Language

El lenguaje de comandos guardado ( GCL ) es un lenguaje definido por Edsger Dijkstra para la semántica de transformadores de predicados . Combina conceptos de programación de forma compacta, antes de que el programa se escriba en algún lenguaje de programación práctico. Su simplicidad facilita la comprobación de la corrección de los programas utilizando la lógica de Hoare .

Comando vigilado

El comando protegido es el elemento más importante del lenguaje de comando protegido. En un comando protegido, tal como lo indica el nombre, el comando está "protegido". La guardia es una proposición , que debe ser verdadera antes de que se ejecute la declaración . Al comienzo de la ejecución de esa declaración, uno puede asumir que la guardia es verdadera. Además, si la guardia es falsa, la declaración no se ejecutará. El uso de comandos protegidos facilita la prueba de que el programa cumple con la especificación . La declaración es a menudo otra orden cautelosa.

Sintaxis

Un comando cauteloso es una declaración de la forma G → S, donde

• G es una proposición , llamada guardia
• S es una declaración

Si G es verdadero, el comando protegido puede escribirse simplemente S.

Semántica

En el momento en que se encuentra G en un cálculo, se evalúa.

• Si G es verdadero, ejecute S
• Si G es falso, mire el contexto para decidir qué hacer (en cualquier caso, no ejecute S)

Saltar y cancelar

Skip y Abort son declaraciones muy simples e importantes en el lenguaje de comandos reservado. Abortar es la instrucción indefinida: haz cualquier cosa. La declaración de aborto ni siquiera necesita terminar. Se utiliza para describir el programa al formular una prueba, en cuyo caso la prueba suele fallar. Omitir es la instrucción vacía: no hacer nada. Se usa en el programa mismo, cuando la sintaxis requiere una declaración, pero el programador no quiere que la máquina cambie de estado .

Sintaxis

skip

abort

Semántica

• Saltar: no hacer nada
• Abortar: hacer cualquier cosa

Asignación

Asigna valores a variables .

Sintaxis

v := E

o

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

dónde

• v son variables de programa
• E son expresiones del mismo tipo de datos que sus correspondientes variables

Concatenación

Las declaraciones están separadas por un punto y coma (;)

Selección : si

La selección (a menudo denominada "instrucción condicional" o "instrucción if") es una lista de comandos protegidos, de los cuales se elige uno para ejecutar. Si más de una guardia es verdadera, una declaración se elige de forma no determinista para ser ejecutada. Si ninguno de los guardias es cierto, el resultado es indefinido. Debido a que al menos uno de los guardias debe ser verdadero, a menudo se necesita la declaración vacía "omitir".

Sintaxis

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

Semántica

Tras la ejecución de una selección, se evalúan todas las protecciones. Si ninguno de los guardias se evalúa como verdadero, la ejecución de la selección se cancela; de lo contrario, uno de los guardias que tiene el valor verdadero se elige de forma no determinista y se ejecuta la instrucción correspondiente.

Ejemplos de

Sencillo

En pseudocódigo :

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

En lenguaje de comando reservado:

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

Uso de saltar

En pseudocódigo:

if error is True then 
  set x to 0

En lenguaje de comando reservado:

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

Si se omite la segunda protección y error = False, el resultado es abortar.

Más guardias verdaderos

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

Si a = b, se elige a o b como el nuevo valor para el máximo, con resultados iguales. Sin embargo, alguien que implemente esto, puede encontrar que uno es más fácil o más rápido que el otro. Dado que no hay diferencia para el programador, es libre de implementar de cualquier manera.

Repetición : hacer

La repetición ejecuta los comandos guardados repetidamente hasta que ninguno de los guardias es verdadero. Por lo general, solo hay un guardia.

Sintaxis

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

Semántica

Tras la ejecución de una repetición, se evalúan todos los guardias. Si todos los guardias evalúan como falso, se ejecuta la omisión. De lo contrario, uno de los guardias que tiene el valor verdadero se elige de forma no determinista y se ejecuta la instrucción correspondiente, después de lo cual se vuelve a ejecutar la repetición.

Ejemplos de

Algoritmo euclidiano original

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

Esta repetición termina cuando a = b, en cuyo caso ayb tienen el máximo común divisor de A y B.

Dijkstra ve en este algoritmo una forma de sincronizar dos ciclos infinitos a := a - by b := b - ade tal manera que a≥0y b≥0sigue siendo cierto.

Algoritmo euclidiano extendido

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 repetición termina cuando b = 0, en cuyo caso las variables tienen la solución a la identidad de Bézout : xA + yB = mcd (A, B).

Tipo no determinista

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

El programa sigue permutando elementos mientras uno de ellos es mayor que su sucesor. Este tipo de burbuja no determinista no es más eficiente que su versión determinista, pero es más fácil de probar: no se detendrá mientras los elementos no estén ordenados y que en cada paso clasifique al 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 encuentra el valor 1 ≤ y ≤ n para el cual una función entera f dada es máxima. No solo el cálculo, sino también el estado final no se determina necesariamente de forma única.

Aplicaciones

Programas correctos por construcción

La generalización de la congruencia observacional de los comandos guardados en una celosía ha llevado al cálculo de refinamiento . Esto se ha mecanizado en métodos formales como el método B que permiten derivar formalmente programas a partir de sus especificaciones.

Circuitos asincrónicos

Los comandos protegidos son adecuados para el diseño de circuitos casi insensibles al retardo porque la repetición permite retardos relativos arbitrarios para la selección de diferentes comandos. En esta aplicación, una puerta lógica que impulsa un nodo y en el circuito consta de dos comandos protegidos, como se indica a continuación:

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

PullDownGuard y PullUpGuard aquí son funciones de las entradas de la puerta lógica, que describen cuando la puerta tira de la salida hacia abajo o hacia arriba, respectivamente. A diferencia de los modelos clásicos de evaluación de circuitos, la repetición de un conjunto de comandos protegidos (correspondientes a un circuito asíncrono) puede describir con precisión todos los posibles comportamientos dinámicos de ese circuito. Dependiendo del modelo con el que uno esté dispuesto a vivir para los elementos del circuito eléctrico, pueden ser necesarias restricciones adicionales en los comandos protegidos para que una descripción del comando protegido sea completamente satisfactoria. Las restricciones comunes incluyen estabilidad, no interferencia y ausencia de comandos autoinvalidables.

Comprobación de modelo

Los comandos protegidos se utilizan dentro del lenguaje de programación Promela , que utiliza el verificador de modelos SPIN . SPIN verifica el funcionamiento correcto de las aplicaciones de software simultáneas.

Otro

El módulo Perl Commands :: Guarded implementa una variante determinista y rectificadora de los comandos guardados de Dijkstra.

Referencias