Especificación: Descripción del problema que queremos resolver.

• ¿Qué problema?
• Usualmente en lenguaje formal.
• Provee propiedades de la solución (output).
• Incluye un conjunto de parámetros (input) que serán conocidos recién al interpretar el programa.

Algoritmo: Descripción de la solución escrita por humanos.

• ¿Cómo resolvemos el problema?

Programa: Descripción de la solución para ser ejecutada en una computadora.

• ¿Cómo resolvemos el problema? descripto en un lenguaje de programación.

Especificación de un problema

proc nombre(parámetros){
	Pre {P}
	Post {Q}
}

Nombre: nombre que le damos al problema. Será resuelto por una función homónima.

Predicados: precondición y postcondición del procedimeinto.

proc sqrt(in x : R, out result : R) {
	Pre {x >= 0}
	Post {result * result = x and result >= 0}
}

Parámetros: lista de parámetros separadas por comas, donde cada parámetro especifica:

• Tipo de pasaje: entrada, salida, entrada y salida.
• Nombre del parámetro
• Tipo de dato

<aside> 💡 Cuando no tenemos precondiciones escribimos Pre {True}

</aside>

Si el usuario suministra datos que hacen verdadera la precondición entonces el programa $P$ termina en una cantidad finita de pasos retornando un valor que hace verdadera la postcondición.

Pasaje de parámetros

<aside> 💡 Todos los parámetros con atributo in (es decir, inclusive inout) están inicializados.

</aside>

1. in: Si se llama al procedimiento con el argumento c para un parámetro de este tipo, antes de iniciar la ejecución se copia el valor c al parámetro en cuestión.

2. out: Al finalizar la ejecución del procedimiento se copia el valor al parámetro pasado. No se inicializan (no podemos mencionarlos en la precondición).

3. inout: Es a la vez de entrada y de salida. La ejecución del procedimiento modifica el valor del parámetro.

   proc incremento(in a : Z, out result : Z) {
   	Pre {True}
   	Post {result = a + 1}
   }
   
   proc incremento(inout a : Z){
   	Pre {a = A_0}
   	Post {a = A_0 + 1}
   }
   

   $A_0$ es una metavariable, representa el valor inicial de a y lo usamos para relacionar en la postcondición el valor de salida de a con su valor inicial.

Riesgos de la especificación

Sobre-especificación

Consiste en dar una postcondición más restrictiva que lo que se necesita, o bien dar una precondición más laxa.

Limita los posibles algoritmos que resuelven el problema.

Sub-especificación

Consiste en dar una precondición más restrictiva que lo realmente necesario, o bien una postcondición más débil que la que podríamos dar.

Deja afuera datos de entrada válidos o ignora condiciones necesarias para la salida.

Lenguaje de especificación

Tipos de datos

Un tipo de datos es un conjunto de valores provisto de una serie de operaciones que involucran a esos valores.

Para hablar de un elemento de un tipo $T$ en nuestro lenguaje escribimos un término o expresión

• Variable de tipo $T$
• Constante de tipo $T$
• Función (operación) aplicada a otros términos (no necesariamente del tipo $T$)

Todos los tipos tiene un elemento distinguido: $\perp$ (bottom) ó Indef que representa ningún valor.