Especificación formal de algoritmos

Vamos a escribir especificaciones claras y precisas. Para ello es necesario un lenguaje formal, llamado así porque tanto su sintaxis como su semántica están perfectamente definidas. Vamos a utilizar una técnica de especificación formal de algoritmos basada en lógica de predicados denominada especificación pre/post.

Sea A un algoritmo del que conocemos sus parámetros de entrada y sus resultados. Una especificación pre/post utiliza un predicado Q, denominado precondición, que incluye como variables libres los parámetros de entrada de A y describe los estados en los que el algoritmo puede ejecutarse.

Además, se utiliza otro predicado R, denominado postcondición, que incluye los parámetros de entrada y los resultados de A. Este predicado R describe los estados finales que el algoritmo alcanza tras su ejecución dando la relación entre la entrada y la salida. La notación

representa la especificación formal de A y ha de leerse como:

“si A comienza su ejecución en un estado que satisface Q, entonces la ejecución de A termina y lo hace en un estado que cumple R”.

Para escribir la precondición y la postcondición, los predicados se podrán construir a partir de fórmulas atómicas (las constantes verdadero y falso, variables booleanas, expresiones aritméticas relacionales como las construidas con las operaciones =, \neq, ≤, etc.), las conectivas lógicas de negación (¬\negP), conjunción (P\wedgeQ), disyunción (P\veeQ) e implicación (P \longrightarrow Q) y los cuantificadores, universal (\forall) y existencial (\exist).

Utilizaremos cuantificadores en los que se indica el rango de la variable cuantificada, r(i), y la expresión a evaluar, E(i), según el siguiente formato:

(Cuantificador i)(E(i) : r(i))

Ejemplos:

Si el rango de un cuantificador universal es vacío, esto es, no hay ningún valor de i que satisfaga el predicado, entonces el predicado es igual a verdadero y en el caso de una cuantificación existencial, el valor es falso. Como se puede ver, en ambos casos, corresponde al elemento neutro de la operación representada.

Para escribir expresiones también utilizaremos otros cuantificadores, siempre indicando el rango de la variable ligada:

Si el rango de un cuantificador es vacío, esto es, no hay ningún valor de i que satisfaga el predicado, entonces el predicado es igual al elemento neutro de la operación representada.

Qn0Q \equiv n \geq0

Funcion FACTORIAL (n:entero) retorna (f:entero) 
    si n = 0 -> 1
    sino n > 0 -> FACTORIAL(n-1) * n
    fsi
ffunción

RR \equiv {f=(i)(i:1in) f=(\prod i)(i:1\le i \le n) }

Last updated