Materia: #algoritmos_y_estructuras_de_datos

Tags:

Especificación

Dentro del mundo de la programación, siempre trabajamos bajo la idea de contrato, en la que alguien nos solicita que diseñemos un programa que lo ayude a realizar una operación concreta. Bajo estos términos, necesitamos aclarar que tipo de problema queremos solucionar y como vamos a poder hacerlo.

Es en este contexto donde nace la idea de especificación, con la cual queremos dejar bien en claro, de manera formal y sin lugar a dudas o interpretaciones, que es lo que hay que resolver. No nos va a decir como hacerlo, pero si nos indica que tipo de parámetros de entrada vamos a utilizar, que salida esperamos, y, sin mas vueltas, que proceso queremos hacer. Esta escritura formal nos será útil a la hora de testear el programa y verificar su correctitud.

Cada parámetro que tenga una especificación va a tener un tipo de dato, lo cual es un conjunto de valores y operaciones que se pueden aplicar sobre esos mismos valores.

Retomando lo del contrato, siempre vamos a tener esta perspectiva. Vamos a trabajar en términos de un usuario que nos solicita a nosotros, los programadores, que diseñemos un programa para solucionar un problema.

Sintaxis

Una especificación consta de varias partes, en particular, se ven mas o menos así:

proc nombreDeLaFuncion(parametros) {
	requiere {precondición}
	asegura {postcondición}
	/*Esto es un comentario, y va a ser ignorado*/
}

Donde proc es una palabra reservada para referirnos a procedimiento, es para iniciar la definición de la especificación. El nombre es el nombre que le damos a nuestra especificación, el cual podemos elegir nosotros. Recomendamos usar nombres claros y que indiquen cual es la operación a resolver. Luego, los parámetros son los valores de entrada o salida que nuestra especificación va a necesitar para realizar su evaluación, suelen escribirse tipados.

Luego, el renglón de requiere, la cual es una palabra reservada para iniciar las precondiciones. Estas van a ser nuestras condiciones que el usuario deberá cumplir con sus valores de entrada. Es decir, nosotros (los programadores) vamos a dar por hecho que estas condiciones se van a cumplir. Es obligación del usuario cumplir siempre con los requiere de nuestro programa.

Finalmente, llegamos a la parte del asegura, que también es una palabra reservada, en este caso inicia las postcondiciones. A diferencia del anterior punto, estas serán las condiciones que nuestro programa deberá cumplir para obtener la correcta salida o solución. Es decir, es obligación del programador asegurar que las postcondiciones se cumplan, y que el programa concluya lo que es correcto.

Por ultimo, y no por eso menos importante, esta el comentario. A la hora de evaluar una especificación esos son ignorados, pero pueden hacer la lectura mucho mas amena.

Una cosa a tener en cuenta es acerca de los parámetros, los cuales tienen tres formas de entrar: $in$, $out$ e $inout$. Esto se suele especificar en la propia sintaxis antes de los parámetros, por ejemplo $in$ $x:\mathbb{Z}$, o lo que es lo mismo $x$ va a ser una variable de entrada de tipo entero. Primero, las variables que se inicializan con el prefijo $in$ son aquellas que solo se puede acceder dentro de la función en la que se creo. El pasaje $out$ hace referencia a que los valores son exclusivamente salida, es decir, parte del resultado o el resultado en cuestión. En definitiva, son variables que se ven afectadas al concluir el programa. Por otro lado, una variable que se inicializa con $inout$, es una variable de entrada pero que su valor se ve alterado o modificado al concluir el programa. No es un nuevo resultado, modificamos el mismo valor de entrada.

Algo útil a tener en cuenta a la hora de trabajar con funciones que tengan parámetros $inout$, es como acceder al valor "viejo" o al "modificado" indistintamente. Para eso usamos la función $old(x)$, que toma una variable $x$ y devuelve el valor inicial de la misma.

Otra cosa importante, es que a la hora de especificar problemas no podemos utilizar otros procedimientos para la solución del mismo. Solo podemos utilizar predicados y funciones auxiliares, obviamente definiéndolos previamente. A su vez, dentro de las funciones auxiliares no podemos definir instrucciones recursivas, ya que solo se tratan de un reemplazo sintáctico.

Funciones auxiliares, predicados y condicionales

Existen ocasiones en las que hay una o mas operaciones que utilizamos reiteradas veces, y puede ser molesto repetirlas, aparte de hacer difícil la futura lectura de la especificación. Para estos casos, tenemos las funciones auxiliares, que son especificaciones mucho mas básicas y sencillas, las cuales hacen una operación exclusiva. La sintaxis de las funciones auxiliares se ve así:

aux nombre (parámetros) : resultado = procedimiento

Se asemeja bastante a lo visto antes, lo único nuevo es aquella parte de procedimiento. Aquí es donde escribiremos la operación a realizar o el resultado a dar. Fíjense que no tenemos ni requiere ni asegura, lo cual hace mucho mas básica esta estructura. Un ejemplo habitual puede ser obtener un valor aproximado de alguna constante matemática, como:

aux pi () : R = 3.14159

Noten que acá hicimos una función que no tiene parámetros de entrada, lo cual también podría aplicarse a las especificaciones habituales.

También, podemos definir predicados, que son operaciones básicas como las funciones auxiliares de antes, pero que exclusivamente evalúan una fórmula lógica, es decir, su resultado es únicamente un valor de verdad. Un ejemplo común de esto puede ser:

pred esPar(n : Z) {
	n mod 2 = 0
}

Finalmente, tenemos las expresiones condicionales, las cuales son funciones que elige entre dos elementos del mismo tipo, según una fórmula lógica. En particular, si la fórmula es verdadera, elije la primera opción, y en caso contrario, la segunda. La estructura de una expresión condicional es del tipo:

if condicion then primer_resultado else segundo_resultado fi