Análisis y Diseño de Algoritmos
Tema 2: Especificación de Programas
Imperativos
Contenido
• Especificación vs Implementación
• Especificación formal: Motivación
• Especificación pre/post
• Predicados lógicos
• Semántica
• Especificación de predicados
• Especificación de problemas
2
Especificación vs Implementación
• La especificación de un algoritmo es la descripción de qué es lo que
hace y bajo qué condiciones lo hace
• La implementación de un algoritmo es la descripción de la
secuencia de instrucciones que hacen que la especificación se
satisfaga. (cómo)
• La especificación de un algoritmo es un paso necesario para su
implementación correcta.
• Una especificación precisa descrita en un lenguaje lógico
matemático permite la demostración de que el algoritmo
implementado satisface la especificación (verificación)
Especificación Implementación
Verificación
3
Especificación vs Implementación
Especificación pre/post Implementación
4
Especificación formal: motivación
• Una posible implementación sería
{a 0, b>0} a = 5, b =2
(1) int q = 0;
(3) a = 5, b =2, q = 0, r = 5
(2) int r = a;
(3) while (r > b){ (4) a = 5, b =2, q = 0, r = 5
Estados
(4) r = r - b; del programa
(5) a = 5, b =2, q = 0, r = 3
(5) q++;
} (3) a = 5, b =2, q = 1, r = 3
{a = qb + r} (4) a = 5, b =2, q = 1, r = 3
(5) a = 5, b =2, q = 1, r = 1
¿Se nos ocurre alguna otra forma (3) a = 5, b =2, q = 2, r = 1
de cumplir la especificación con
a = 5, b =2, q = 2, r = 1
una implementación distinta?
5
Especificación formal: motivación
{a 0, b>0} a = 6, b =2
(1) int q = 0;
(3) a = 6, b =2, q = 0, r = 6
(2) int r = a;
(3) while (r > b){ (4) a = 6, b =2, q = 0, r = 6
(4) r = r - b;
(5) a = 6, b =2, q = 0, r = 4
(5) q++;
} (3) a = 6, b =2, q = 1, r = 4
{a = qb + r} (4) a = 6, b =2, q = 1, r = 4
(5) a = 6, b =2, q = 1, r = 2
(3) a = 6, b =2, q = 2, r = 2
La división no
está bien calculada a = 6, b =2, q = 2, r = 2 ???
6
Especificación formal: motivación
a = 6, b =2
(3) a = 6, b =2, q = 0, r = 6
{a 0, b>0}
(1) int q = 0; (4) a = 6, b =2, q = 0, r = 6
(2) int r = a; (5) a = 6, b =2, q = 0, r = 4
(3) while (r >= b){
(4) r = r - b; (3) a = 6, b =2, q = 1, r = 4
(5) q++; (4) a = 6, b =2, q = 1, r = 4
}
(5) a = 6, b =2, q = 1, r = 2
{a = qb + r, r < b}
(3) a = 6, b =2, q = 2, r = 2
Modificamos el aserto (4) a = 6, b =2, q = 2, r = 2
(postcondición).
(5) a = 6, b =2, q = 2, r = 0
(3) a = 6, b =2, q = 3, r = 0
a = 6, b =2, q = 3, r = 0
7
Especificación formal: motivación
{a 0, b>0}
(1) int q = 0;
(2) int r = a; Si hubiéramos especificado
(3) while (r >= b){ correctamente el resultado,
(4) r = r - b; seguramente el código se
habría implementado
(5) q++;
correctamente desde el
} principio
{a = qb + r, r < b}
¿Funciona este algoritmo para una precondición distinta?
8
Especificación pre/post
a = 5, b =2
{a 0, b>0} a = 5, b =2, q = 0, r = 5
(1) int q = 0; a = 5, b =2, q = 0, r = 5
(2) int r = a; Estados del programa
a = 5, b =2, q = 0, r = 3
(3) while (r >= b){
a = 5, b =2, q = 1, r = 3
(4) r = r - b;
(5) q++; a = 5, b =2, q = 1, r = 3
} a = 5, b =2, q = 1, r = 1
{a = qb + r,r < b} a = 5, b =2, q = 2, r = 1
a = 5, b =2, q = 2, r = 1
La ejecución de un programa puede definirse como una secuencia de estados
9
Especificación pre/post
a = 5, b =2
{a 0, b>0} a = 5, b =2, q = 0, r = 5
(1) int q = 0; a = 5, b =2, q = 0, r = 5
Asertos
(2) int r = a;
a = 5, b =2, q = 0, r = 3
(3) while (r >= b){
a = 5, b =2, q = 1, r = 3
(4) r = r - b;
(5) q++; a = 5, b =2, q = 1, r = 3
} a = 5, b =2, q = 1, r = 1
{a = qb + r,r < b} a = 5, b =2, q = 2, r = 1
a = 5, b =2, q = 2, r = 1
10
Especificación pre/post
11
Predicados lógicos
12
Semántica
13
Especificación de problemas
14
Especificación de problemas
/**
* @param a array arbitrario
* @return max el mayor valor
*/
/ / pre{[Link] > 0}
int maximo(int[] a)
/ / post{$0 £ j < [Link] : (max = a[ j], "0 £ i < [Link] : a[ j] ³ a[i])
/**
* @param a array arbitrario
* @return b = true, si alguna de sus componentes es igual a la suma
* de las que la preceden, o b = false, en otro caso
*/
/ / pre{[Link] > 0}
boolean suma(int[] a)
j-1
/ / post{b = ($0 £ j < [Link] : (a[ j] = å a[i]))}
i=0
15
Referencias
• Diseño de Programas: Formalismo y Abstracción.
R. Peña. Ed. Prentice-Hall
• The Science of Programming. D. Gries. Ed.
Springer-Verlag
16
En Java
/**
* Devuelve un BigInteger cuyo valor es él mismo a la inversa modulo m
* @param m el módulo.
* @throws ArithmeticException si m <= 0
*/
public BigInteger modInverse(BigInteger m) {
if ([Link] <= 0)Q
throw new ArithmeticException("Modulus not positive:“+m);
// Secuencia de instrucciones que calcula el resultado en la
//variable result
assert [Link](result).mod(m).equals(ONE) : this;
return result; R
}
17
