Hispanopedia WikiEl lenguaje de comandos protegidos ( 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 de forma conjunta, con las ideas de la demostración como guía; además, partes de un programa pueden calcularse .
Una propiedad importante de GCL es el no determinismo . Por ejemplo, en la instrucción `if`, varias alternativas pueden ser verdaderas, y la elección se realiza en tiempo de ejecución, cuando se ejecuta la instrucción. Esto libera al programador de tener que tomar decisiones innecesarias y facilita el desarrollo formal de programas.
GCL incluye la instrucción de asignación múltiple. Por ejemplo, la ejecución de la instrucción 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 instrucción intercambia los valores de x e y .
Los siguientes libros tratan sobre el desarrollo de programas utilizando GCL :
- Dijkstra, Edsger W. (1976). Una disciplina de programación . Prentice Hall. ISBN 978-0132158718.
- Gries, D. (1981). La ciencia de la programación . Monografías en informática (en inglés, español, japonés, chino, italiano y ruso). Nueva York: Springer Verlag. doi : 10.1007/978-1-4612-5983-1 . ISBN 978-0-387-96480-5. S2CID 37034126 .
- Dijkstra, Edsger W .; Feijen, Wim HJ (1988). Un método de programación . Boston, MA: Addison-Wesley Longman Publishing Co., Inc. p. 200.ISBN 978-0-201-17536-3.
- Kaldewaij, Anne (1990). Programación: la derivación de algoritmos . Prentice-Hall, Inc. ISBN 0132041081.
- Cohen, Edward (1990). David Gries (ed.). Programación en la década de 1990: Una introducción al cálculo de programas . Textos y monografías en informática. Springer Verlag. doi : 10.1007/978-1-4613-9706-9 . ISBN 978-1-4613-9706-9. S2CID 1509875 .
Comando vigilado
Un comando con protección consta de una condición booleana o protección y una instrucción "protegida" por ella. La instrucción solo se ejecuta si la protección es verdadera, por lo que, al analizar la instrucción, se puede asumir que la condición es verdadera. Esto facilita demostrar que el programa cumple con una especificación .
Un comando protegido es una declaración de la forma G → S, donde
- G es una proposición , llamada guardia
- S es una declaración
- Si G se evalúa como verdadero, S puede ejecutarse. En la mayoría de las construcciones de GCL, varios comandos con condiciones pueden tener condiciones verdaderas, y se elige arbitrariamente exactamente una de ellas para su ejecución.
- Si G es falso, S no se ejecutará.
saltar y abortar
Las instrucciones `skip` y `abort` son importantes en el lenguaje de comandos protegido. `abort` es la instrucción indefinida: no hace nada. Ni siquiera necesita terminar. Se usa para describir el programa al formular una demostración, en cuyo caso la demostración suele fallar. `skip` es la instrucción vacía: no hace nada. Se usa a menudo cuando la sintaxis requiere una instrucción, pero el estado no debe cambiar.
Sintaxis
saltar
abortar
Semántica
- saltar : no hacer nada
- abortar : hacer cualquier cosa
Asigna valores a las variables .
Sintaxis
v := E
o
v 0 , v 1 , ..., v norte := mi 0 , mi 1 , ..., mi norte
dónde
- v son variables de programa
- E son expresiones del mismo tipo de datos que sus variables correspondientes.
Cadena
Las instrucciones están separadas por un punto y coma (;).
Selección : si
La selección (a menudo llamada "sentencia condicional" o "sentencia if") es una lista de comandos protegidos, de los cuales se elige uno para ejecutar. Si más de una condición es verdadera, se elige arbitrariamente una instrucción cuya condición sea verdadera para ejecutarse. Si ninguna condición es verdadera, el resultado es indefinido, es decir, equivalente a abortar . Debido a que al menos una de las condiciones debe ser verdadera, a menudo se necesita la instrucción vacía skip . La instrucción if fi no tiene comandos protegidos, por lo que nunca hay una condición verdadera. Por lo tanto, if fi es equivalente a abortar .
Sintaxis
si G0 → S0 □ G1 → S1 ... □ Gn → Sn fi
Semántica
Al ejecutar una selección, se evalúan las condiciones. Si ninguna de las condiciones es verdadera , la selección se interrumpe; de lo contrario, se elige arbitrariamente una de las cláusulas con una condición verdadera y se ejecuta su instrucción.
Implementación
GCL no especifica una implementación. Dado que las condiciones de guarda no pueden tener efectos secundarios y la elección de la cláusula es arbitraria, una implementación puede evaluar las condiciones de guarda en cualquier secuencia y elegir la primera cláusula verdadera , por ejemplo.
Ejemplos
Simple
En pseudocódigo :
Si a < b, entonces establece c en verdadero. de lo contrario, establezca c en Falso
En lenguaje de comandos protegido:
Si a < b → c := verdadero □ a ≥ b → c := falso fi
Uso de omitir
En pseudocódigo:
Si el error es verdadero, entonces establezca x en 0.
En lenguaje de comandos protegido:
Si hay un error, x := 0 □error → omitir fi
Si se omite la segunda protección y el error es falso, el resultado es la interrupción.
Más guardias de verdad
si a ≥ b → max := a □ b ≥ a → max := b fi
Si a = b, se elige a o b como nuevo valor para el máximo, obteniéndose resultados iguales. Sin embargo, la implementación puede determinar que una opción es más sencilla o rápida que la otra. Dado que para el programador no hay diferencia, cualquier implementación es válida.
Repetición : hacer
La ejecución de esta repetición, o bucle, se muestra a continuación.
Sintaxis
hacer G0 → S0 □ G1 → S1 ... □ Gn → Sn sobredosis
Semántica
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 comando protegido Gi es verdadero y ejecutar el comando Si . Por lo tanto, si todos los comandos protegidos 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 .
Ejemplos
Algoritmo euclidiano original
a, b := A, B; hacer a < b → b := b - a □ b < a → a := a - b sobredosis
Esta repetición termina cuando a = b, en cuyo caso a y b son el máximo común divisor de A y B.
Dijkstra ve en este algoritmo una forma de sincronizar dos ciclos infinitos de tal manera que y permanece verdadero.a := a - bb := b - aa≥0b≥0
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*v sobredosis
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).
Ordenación no determinista
hacer a>b → a, b := b, a □ b>c → b, c := c, b □ c>d → c, d := d, c sobredosis
El programa continúa permutando elementos mientras uno de ellos sea mayor que su sucesor. Este algoritmo de 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 ordena al menos dos 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 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 están necesariamente determinados de forma única.
Aplicaciones
Programas correctos por diseño
La generalización de la congruencia observacional de comandos protegidos en una red ha dado lugar 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.
circuitos asíncronos
Los comandos protegidos son adecuados para el diseño de circuitos prácticamente insensibles al retardo, ya que la repetición permite retardos relativos arbitrarios para la selección de diferentes comandos. En esta aplicación, una puerta lógica que controla un nodo y en el circuito consta de dos comandos protegidos, como se muestra a continuación:
PullDownGuard → y := 0 PullUpGuard → y := 1
PullDownGuard y PullUpGuard son funciones de las entradas de la puerta lógica que describen cuándo la puerta baja o sube la salida, 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 comportamientos dinámicos posibles de dicho circuito. Dependiendo del modelo que se esté dispuesto a utilizar para los elementos del circuito eléctrico, pueden ser necesarias restricciones adicionales en los comandos protegidos para que la descripción sea completamente satisfactoria. Las restricciones comunes incluyen estabilidad, ausencia de interferencias y ausencia de comandos autoinvalidantes. [ 3 ]
Verificación de modelos
Los comandos protegidos se utilizan en el lenguaje de programación Promela , que es el que utiliza el verificador de modelos SPIN . SPIN verifica el correcto funcionamiento de las aplicaciones de software concurrentes.
Otro
El módulo Perl Commands::Guarded implementa una variante determinista y rectificadora de los comandos protegidos de Dijkstra.
Referencias
- ↑ Dijkstra, Edsger W. " EWD472: Comandos protegidos, no determinismo y derivación formal de programas" (PDF) . Consultado el 16 de agosto de 2006 .
- ↑ Back, Ralph J (1978). "Sobre la corrección de los pasos de refinamiento en el desarrollo de programas (tesis doctoral)" (PDF) . Archivado del original (PDF) el 20 de julio de 2011.
- ↑ Martin, Alain J. "Síntesis de circuitos VLSI asíncronos" .
- Programación lógica
- Edsger W. Dijkstra
