title: Lenguaje de Comandos Guardados
text: # Lenguaje de 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.
  
  # Lenguaje de Comandos Guardados
  ## Comando guardado
  
  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.
  
  # Lenguaje de Comandos Guardados
  ## Comando guardado
  ### Sintaxis
  
  Un comando guardado es un enunciado de la forma $G\rightarrow S$, donde
  * $G$ es la proposición de guarda;
  * $S$ es una instrucción.
  
  # Lenguaje de Comandos Guardados
  ## Comando guardado
  ### Semántica
  
  Cuando $G$ se encuentra en un cálculo, se evalúa.
  * Si $G$ es verdadero, se ejecuta $S$.
  * Si $G$ es falso, lo que se hará dependerá del contexto.
  Las sentencias $G$ pueden cambiar estados:
      x, z = y, y + 1 el nuevo valor de x es y y el nuevo valor de z es y + 1
  o realizar entrada y salida:
      print "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:
      true $\rightarrow$ print 5
  es equivalente a:
      print 5
  
  # Lenguaje de Comandos Guardados
  ## Skip y Abort
  
  Skip y Abort son enunciados simples pero importantes en el lenguaje de comandos guardados.
  * Abort es la instrucción indefinida: hacer cualquier cosa. El enunciado Abort no tiene por qué implicar la terminación (aborto) del programa; se usa para describir el programa al formular una demostración, en cuyo caso la demostración generalmente falla.
  * Skip es la instrucción vacía: no hacer nada. Se usa en el programa en sí mismo, cuando la sintaxis requiere un enunciado y el programador no quiere que la máquina cambie estados.
  
  # Lenguaje de Comandos Guardados
  ## La construcción condicional if
  
  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.
  
  # Lenguaje de Comandos Guardados
  ## La construcción condicional if
  ### Sintaxis
  
      ${\mbox{if}}$
         $G_{0}\rightarrow S_{0}$
         $\ G_{1}\rightarrow S_{1}$
         $\ G_{n}\rightarrow S_{n}$
      ${\mbox{fi}}$
  
  # Lenguaje de Comandos Guardados
  ## La construcción condicional if
  ### Semántica
  
  * Si ninguna de las guardas es verdadera: Abort;
  * Si solamente la guarda $G_{x}$ es verdadera: ejecutar $S_{x}$;
  * Si las guardas $G_{x_{0}}\ ...\ G_{x_{m}}$ son verdaderas: ejecutar cualquier $S_{x_{y}}$, donde $0\leq y\leq m$
  
  # Lenguaje de Comandos Guardados
  ## La construcción condicional if
  ### Ejemplo
  
  Dada la expresión en pseudocódigo:
      if $a\geq b$ then print "Mayor ó igual";
      else if $a<b$ then print "Menor";
  El equivalente en comandos guardados es:
      if
         $a\geq b\rightarrow$ print "Mayor ó igual"
         $a<b\rightarrow$ print "Menor"
      fi
  La potencia de los comandos guardados se ilustra en la siguiente expresión:
      if
         $a\geq b\rightarrow$ print "Mayor ó igual"
         $a\leq b\rightarrow$ print "Menor ó igual"
      fi
  Cuando $a=b$, el resultado del comando puede ser o bien "Mayor ó igual" o bien "Menor ó igual" (pero no los dos).
  
  # Lenguaje de Comandos Guardados
  ## La construcción de bucle do
  
  La construcción de repetición do se escribe así:
      ${\mbox{do}}$
         $G_{0}\rightarrow S_{0}$
         $\ G_{1}\rightarrow S_{1}$
         $\ G_{n}\rightarrow S_{n}$
      ${\mbox{od}}$
  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).
  
  # Lenguaje de Comandos Guardados
  ## La construcción de bucle do
  ### Ejemplo
  
  A continuación se da una implementación del algoritmo de Euclides para hallar el máximo común divisor.
      x, y = X, Y
      do de nuevo, terminación cuando $x=y$
         $x>y\rightarrow$ x:= x-y
         $y>x\rightarrow$ y:= y-x
      od
      print x
  
  # Lenguaje de Comandos Guardados
  ## Aplicaciones
  ### Circuitos Asíncronos
  
  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\rightarrow y:=0$
      $PullupGuard\rightarrow y:=1$
  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.
  
  # Lenguaje de Comandos Guardados
  ## Implementaciones
  
  Algunas implementaciones de lenguaje de comandos guardados:
  * GaCeLa es una aproximación a un compilador verificante que genera programas que deben cumplir con su especificación, de lo contrario son interrumpidos durante su ejecución. Esta notación (y su correspondiente traductor al lenguaje Java) está siendo desarrollada en la Universidad Simón Bolívar en Venezuela.
  * GCL 1.2, escrita en Prolog y C.