El lenguaje de comandos guardados ( GCL ) es un lenguaje de programación definido por Edsger Dijkstra para la semántica de transformadores de predicados en EWD472. [1] Combina conceptos de programación de forma compacta. Facilita el desarrollo de un programa y su demostración en paralelo, con las ideas de demostración a la cabeza; además, es posible calcular partes de un programa .
Una propiedad importante de GCL es el no determinismo . Por ejemplo, en la sentencia if, varias alternativas pueden ser verdaderas y la elección de cuál elegir se realiza en tiempo de ejecución, cuando se ejecuta la sentencia if. Esto libera al programador de tener que tomar decisiones innecesarias y es una ayuda en el desarrollo formal de programas.
GCL incluye la sentencia de asignación múltiple. Por ejemplo, la ejecución de la sentencia x, y:= y, xse realiza evaluando primero los valores del lado derecho y luego almacenándolos en las variables del lado izquierdo. Por lo tanto, esta sentencia intercambia los valores de x e y .
Los siguientes libros tratan sobre el desarrollo de programas utilizando GCL :
Un comando protegido consta de una condición booleana o protección y una declaración "protegida" por ella. La declaración solo se ejecuta si la protección es verdadera, por lo que al razonar sobre la declaración, se puede asumir que la condición es verdadera. Esto hace que sea más fácil demostrar que el programa cumple con una especificación .
Una orden vigilada es una declaración de la forma G → S, donde
skip y abort son instrucciones importantes en el lenguaje de comandos protegidos. abort es la instrucción indefinida: hacer cualquier cosa. Ni siquiera necesita terminar. Se utiliza para describir el programa al formular una prueba, en cuyo caso la prueba generalmente falla. skip es la instrucción vacía: no hacer nada. Se utiliza a menudo cuando la sintaxis requiere una declaración pero el estado no debe cambiar.
saltar
abortar
Asigna valores a las variables .
v := mi
o
v 0 , v 1 , ..., v norte := mi 0 , mi 1 , ..., mi norte
dónde
Las declaraciones están separadas por un punto y coma (;)
La selección (a menudo llamada "declaración condicional" o "declaración if") es una lista de comandos protegidos, de los cuales se elige uno para ejecutar. Si más de un protector es verdadero, se elige arbitrariamente para ejecutar una declaración cuyo protector sea verdadero. Si ningún protector es verdadero, el resultado es indefinido, es decir, equivalente a abort . Debido a que al menos uno de los protectores debe ser verdadero, a menudo se necesita la declaración vacía skip . La declaración if fi no tiene comandos protegidos, por lo que nunca hay un protector verdadero. Por lo tanto, if fi es equivalente a abort .
si G0 → S0 □ G1 → S1... □ Gn → Snen fin
Al ejecutar una selección, se evalúan las protecciones. Si ninguna de las protecciones es verdadera , se cancela la selección; de lo contrario, se elige arbitrariamente una de las cláusulas con una protección verdadera y se ejecuta su declaración.
GCL no especifica una implementación. Dado que las protecciones no pueden tener efectos secundarios y la elección de la cláusula es arbitraria, una implementación puede evaluar las protecciones en cualquier secuencia y elegir la primera cláusula verdadera , por ejemplo.
En pseudocódigo :
Si a < b, entonces establezca c como VerdaderoDe lo contrario, establezca c en Falso
En lenguaje de comando protegido:
si a < b → c := verdadero □ a ≥ b → c := falsoen fin
En pseudocódigo:
Si el error es Verdadero, establezca x en 0
En lenguaje de comando protegido:
si error → x := 0 □ error → saltar fiSi se omite la segunda protección y el error es Falso, el resultado es aborto.
si a ≥ b → máx := a □ b ≥ a → máx := ben fin
Si a = b, se elige a o b como nuevo valor para el máximo, con resultados iguales. Sin embargo, la implementación puede determinar que uno es más fácil o más rápido que el otro. Como no hay diferencia para el programador, cualquier implementación servirá.
La ejecución de esta repetición o bucle se muestra a continuación.
hacer G0 → S0 □ G1 → S1... □ Gn → Snsobredosis
La ejecución de la repetición consiste en ejecutar 0 o más iteraciones , donde una iteración consiste en elegir arbitrariamente un comando protegido Gi → Si cuyo protector Gi es verdadero y ejecutar el comando Si . Por lo tanto, si todos los protectores son inicialmente falsos, la repetición termina inmediatamente, sin ejecutar una iteración. La ejecución de la repetición do od , que no tiene comandos protegidos, ejecuta 0 iteraciones, por lo que do od es equivalente a skip .
a, b := A, B; hacer a < b → b := b - a □ b < a → a := a - bsobredosis
Esta repetición termina cuando a = b, en cuyo caso a y b 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≥0siga siendo verdadero.
a, b, x, y, u, v := A, B, 1, 0, 0, 1; hacer 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*vsobredosis
Esta repetición termina cuando b = 0, en cuyo caso las variables contienen la solución de la identidad de Bézout : xA + yB = mcd(A,B).
hacer a>b → a, b := b, a □ b>c → b, c := c, b □ c>d → c,d := d,csobredosis
El programa continúa permutando elementos mientras uno de ellos sea mayor que su sucesor. Esta ordenación de burbuja no determinista no es más eficiente que su versión determinista, pero es más fácil de demostrar: no se detendrá mientras los elementos no estén ordenados y en cada paso ordenará al menos 2 elementos.
x, y = 1, 1; hacer x≠n → si f(x) ≤ f(y) → x := x+1 □ f(x) ≥ f(y) → y := x; x := x+1 Fio od
Este algoritmo encuentra el valor 1 ≤ y ≤ n para el cual una función entera dada f es máxima. No solo el cálculo, sino también el estado final no están necesariamente determinados de manera única.
La generalización de la congruencia observacional de los comandos guardados en una red ha llevado al cálculo de refinamiento . [2] Esto se ha mecanizado en métodos formales como el método B que permiten derivar formalmente programas a partir de sus especificaciones.
Los comandos protegidos son adecuados para el diseño de circuitos casi insensibles a los retardos , ya que la repetición permite retardos relativos arbitrarios para la selección de diferentes comandos. En esta aplicación, una compuerta lógica que controla un nodo y en el circuito consta de dos comandos protegidos, como se indica a continuación:
PullDownGuard → y := 0PullUpGuard → y := 1
PullDownGuard y PullUpGuard son funciones de las entradas de la compuerta lógica, que describen cuándo la compuerta baja o sube la salida, respectivamente. A diferencia de los modelos de evaluación de circuitos clásicos, la repetición de un conjunto de comandos protegidos (que corresponden a un circuito asincrónico) puede describir con precisión todos los comportamientos dinámicos posibles de ese circuito. Según el modelo con el que uno esté dispuesto a vivir para los elementos del circuito eléctrico, pueden ser necesarias restricciones adicionales sobre los comandos protegidos para que una descripción de comando protegido sea completamente satisfactoria. Las restricciones comunes incluyen estabilidad, no interferencia y ausencia de comandos autoinvalidantes. [3]
Los comandos protegidos se utilizan dentro del lenguaje de programación Promela , que es utilizado por el verificador de modelos SPIN . SPIN verifica el correcto funcionamiento de aplicaciones de software concurrentes.
El módulo Perl Commands::Guarded implementa una variante determinista y rectificadora de los comandos guardados de Dijkstra.
