Lenguaje de Comandos Guardados

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 ${\displaystyle G\rightarrow S}$ , donde

• ${\displaystyle G}$  es la proposición de guarda;
• ${\displaystyle S}$  es una instrucción.

Cuando ${\displaystyle G}$  se encuentra en un cálculo, se evalúa.

• Si ${\displaystyle G}$  es verdadero, se ejecuta ${\displaystyle S}$ .
• Si ${\displaystyle G}$  es falso, lo que se hará dependerá del contexto.

Las sentencias ${\displaystyle 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 ${\displaystyle \rightarrow }$  print 5

es equivalente a:

print 5

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.

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.

${\displaystyle {\mbox{if}}}$ 

${\displaystyle G_{0}\rightarrow S_{0}}$ 

${\displaystyle []\ G_{1}\rightarrow S_{1}}$ 

${\displaystyle ...}$ 

${\displaystyle []\ G_{n}\rightarrow S_{n}}$ 

${\displaystyle {\mbox{fi}}}$ 

• Si ninguna de las guardas es verdadera: Abort;
• Si solamente la guarda ${\displaystyle G_{x}}$  es verdadera: ejecutar ${\displaystyle S_{x}}$ ;
• Si las guardas ${\displaystyle G_{x_{0}}\ ...\ G_{x_{m}}}$  son verdaderas: ejecutar cualquier ${\displaystyle S_{x_{y}}}$ , donde ${\displaystyle 0\leq y\leq m}$ 

Dada la expresión en pseudocódigo:

if ${\displaystyle a\geq b}$  then print "Mayor ó igual";

else if ${\displaystyle a<b}$  then print "Menor";

El equivalente en comandos guardados es:

if

${\displaystyle a\geq b\rightarrow }$  print "Mayor ó igual"

${\displaystyle a<b\rightarrow }$  print "Menor"

fi

La potencia de los comandos guardados se ilustra en la siguiente expresión:

if

${\displaystyle a\geq b\rightarrow }$  print "Mayor ó igual"

${\displaystyle a\leq b\rightarrow }$  print "Menor ó igual"

fi

Cuando ${\displaystyle a=b}$ , 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í:

${\displaystyle {\mbox{do}}}$ 

${\displaystyle G_{0}\rightarrow S_{0}}$ 

${\displaystyle []\ G_{1}\rightarrow S_{1}}$ 

${\displaystyle ...}$ 

${\displaystyle []\ G_{n}\rightarrow S_{n}}$ 

${\displaystyle {\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).

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 ${\displaystyle x=y}$ 

${\displaystyle x>y\rightarrow }$  x:= x-y

${\displaystyle y>x\rightarrow }$  y:= y-x

od

print x

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:

${\displaystyle PulldownGuard\rightarrow y:=0}$ 

${\displaystyle 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.

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.