Comandos guardados
El Lenguaje de Comandos Guardados (GCL, Guarded Command Language), o de Órdenes Guardadas, es un modelo de lenguaje definido por Edsger Dijkstra para semántica de transformación de predicados (una extensión lógica diseñada para proporcionar una metodología para desarrollar programas "correctos por construcción" en un lenguaje imperativo).
Tiene un conjunto especial de construcciones de condición y de bucle. El elemento más básico del lenguaje es el comando guardado o comando con guarda.
Un comando guardado consiste en una orden —un enunciado— que está "guardada" (protegida) por una proposición llamada guarda, cuyo valor debe ser verdadero antes de que se ejecute el comando. Cuando el enunciado se ejecuta, puede asumirse que la proposición de guarda es verdadera. Si la proposición de guarda es falsa, no se ejecutará el enunciado.
El uso de comandos guardados facilita la comprobación de que el programa cumple la especificación.
Un comando guardado es un enunciado de la forma , donde
Cuando se encuentra en un cálculo, se evalúa.
Las sentencias pueden cambiar estados:
o realizar entrada y salida:
Naturalmente, una implementación de comandos guardados puede permitir cualquier anchura para las condiciones y sentencias.
Un comando guardado se puede presentar por sí solo como una sentencia; en comandos que siempre se ejecutan, la guarda se puede omitir:
es equivalente a:
Skip y Abort son enunciados simples pero importantes en el lenguaje de comandos guardados.
La construcción condicional o de selección es una lista de comandos guardados, de los cuales uno es escogido para ser ejecutado. Si más de una guarda es verdadera, el enunciado que se ejecutará se escoge de forma aleatoria o de forma no determinista. Si ninguna guarda es verdadera, el resultado es indefinido (semánticamente equivalente a una instrucción Abort). Ya que al menos una guarda ha de ser verdadera, es frecuente que se necesite la instrucción Skip.
Dada la expresión en pseudocódigo:
El equivalente en comandos guardados es:
La potencia de los comandos guardados se ilustra en la siguiente expresión:
Cuando , el resultado del comando puede ser o bien "Mayor ó igual" o bien "Menor ó igual" (pero no los dos).
La construcción de repetición do se escribe así:
Las guardas de los comandos guardados se evalúan. Si una de ellas es verdadera, se ejecuta el enunciado correspondiente. Si más de una es verdadera, se ejecuta sólo un enunciado escogido de entre los correspondientes de forma aleatoria o no determinista. El proceso se repite hasta que ninguna de las guardas evalúe como verdadera (es decir, después de ejecutar un comando se vuelve a evaluar las guardas desde el principio).
A continuación se da una implementación del algoritmo de Euclides para hallar el máximo común divisor.
Los comandos guardados son adecuados para diseño de circuitos QDI porque la construcción do-od permite retrasos relativos arbitrarios para la selección de comandos diferentes. En esta aplicación, una puerta lógica manejando un nodo y en el circuito consiste en dos comandos guardados, como sigue:
PulldownGuard y PullupGuard son funciones de la entrada de la puerta lógica, que describen las acciones de salida pull down y pull up respectivamente.
Al contrario que modelos clásicos de evaluación de circuitos, el modelo do-od para un conjunto de comandos guardados (correspondiendo a un circuito asíncrono) puede describir con precisión todos los posibles comportamientos dinámicos del circuito.
Algunas implementaciones de lenguaje de comandos guardados: