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).[1]

Tiene un conjunto especial de construcciones de condición y de bucle. El elemento más básico del lenguaje es el comando guardado ó comando con guarda.

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.

Sintaxis

Un comando guardado es un enunciado de la forma , donde

  • es la proposición de guarda;
  • es una instrucción.

Semántica

Cuando se encuentra en un cálculo, se evalúa.

  • Si es verdadero, se ejecuta .
  • Si es falso, lo que se hará dependerá del contexto.

Las sentencias 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í sólo como una sentencia; en comandos que siempre se ejecutan, la guarda se puede omitir:

true print 5

es equivalente a:

print 5
Other Languages
Nederlands: GCL