PDF de programación - Capítulo 2 - Especificación de algoritmos

Imágen de pdf Capítulo 2 - Especificación de algoritmos

Capítulo 2 - Especificación de algoritmosgráfica de visualizaciones

Publicado el 9 de Julio del 2019
275 visualizaciones desde el 9 de Julio del 2019
161,5 KB
11 paginas
Creado hace 4a (02/10/2015)
Especificación de algoritmos 1

Capítulo 2

Las matemáticas son el alfabeto con el cual Dios
ha escrito el Universo.

Galileo Galilei (1564-1642)

Resumen: En este tema se enseña a distinguir entre especificar e implementar algo-
ritmos, se repasa la lógica de predicados, y se establecen convenios y notaciones para
especificar funciones y procedimientos utilizando dicha lógica.

1.

Introducción









Especificar un algoritmo consiste en contestar a la pregunta “qué hace el algoritmo”,
sin dar detalles sobre cómo consigue dicho efecto. Una actitud correcta consiste en
contemplar el algoritmo como una caja negra de la que solo podemos observar sus
entradas y sus salidas.

Implementar, por el contrario, consiste en contestar a este segundo aspecto, es decir
“cómo se consigue la funcionalidad pretendida”, suponiendo que dicha funcionalidad
está perfectamente clara en la especificación.

Muchos programadores noveles tienen dificultades para distinguir entre ambas activi-
dades, produciendo documentos donde se mezclan continuamente los dos conceptos.

La especificación de un algoritmo tiene un doble destinatario:

Los usuarios del algoritmo: debe recoger todo lo necesario para un uso correcto
del mismo. En particular, ha de detallar las obligaciones del usuario al invocar
dicho algoritmo y el resultado producido si es invocado correctamente.

El implementador del algoritmo: define los requisitos que cualquier implemen-
tación válida debe satisfacer, es decir las obligaciones del implementador. Ha de
dejar suficiente libertad para que este elija la implementación que estime más
adecuada con los recursos disponibles.

1Ricardo Peña es el autor principal de este tema.

13

14



Capítulo 2. Especificación de algoritmos

Una vez establecida la especificación, los trabajos del usuario y del implementador
pueden proseguir por separado. La especificación actúa pues como una barrera o
contrato que permite independizar los razonamientos de corrección de los distintos
componentes de un programa grande. Así, se descompone la tarea de razonar sobre
el mismo en unidades manejables que corresponden a su estructura modular.



Propiedades de una buena especificación:

Precisión Ha de responder a cualquier pregunta sobre el uso del algoritmo sin tener
que acudir a la implementación del mismo. El lenguaje natural no permite la
precisión requerida si no es sacrificando la brevedad.

Brevedad Ha de ser significativamente más breve que el código que especifica. Los

lenguajes formales ofrecen a la vez precisión y brevedad.

Claridad Ha de transmitir la intuición de lo que se pretende. A veces el lenguaje

formal ha de ser complementado con explicaciones informales.



En este capítulo se presenta una técnica de especificación formal de funciones y
procedimientos basada en el uso de la lógica de predicados, también conocida
como técnica pre/post. Más adelante se presentará otra técnica formal diferente,
las llamadas especificaciones algebraicas, más apropiadas para especificar tipos
de datos.



Las ventajas de una especificación formal frente a una informal son bastantes:

Eliminan ambigüedades que el usuario y el implementador podrían resolver
de formas distintas, dando lugar a errores de uso o de implementación que
aparecerían en ejecución.

Son las únicas que permiten realizar una verificación formal del algoritmo.
Este tema se tratará en los capítulos 3 y 4, y consiste en esencia en razonar
sobre la corrección del algoritmo mediante el uso de la lógica.

Permite generar automáticamente un conjunto de casos de prueba que
permitirán probar la corrección de la implementación. La especificación formal
se usa para predecir y comprobar el resultado esperado.



Supongamos declarado en alguna parte el siguiente tipo de datos:

typedef int vect [1000];

(2.1)

Queremos una función que, dado un vector a de tipo vect y un entero n, devuelva un
valor booleano b que indique si el valor de alguno de los elementos a[0], . . . , a[n − 1]
es igual a la suma de todos los elementos que le preceden en el vector. Utilizaremos
la siguiente cabecera sintáctica:

fun essuma (vect a, int n) return (bool b)



Esta especificación informal presenta algunas ambigüedades:

No quedan claras todas las obligaciones del usuario: (1) ¿serían admisibles lla-
madas con valores negativos de n?; (2) ¿y con n = 0?; (3) ¿y con n > 1000?

En caso afirmativo, ¿cuál ha de ser el valor devuelto por la función?

Estructura de Datos y Algoritmos

2. Predicados

15

Tampoco están claras las obligaciones del implementador. Por ejemplo, si n ≥ 1
y a[0] = 0 la función, ¿ha de devolver true o false?

Tratar de explicar en lenguaje natural todas estas situaciones llevaría a una especi-
ficación más extensa que el propio código de la función essuma.



La siguiente especificación formal contesta a estas preguntas:

Q ≡ {0 ≤ n ≤ 1000}
fun essuma (vect a, int n) return bool b
R ≡ {b = ∃w : 0 ≤ w < n : a[w] = (P u : 0 ≤ u < w : a[u])}

No son correctas llamadas con valores negativos de n, ni con n > 1000; sí son correctas
llamadas con n = 0 y en ese caso ha de devolver false; las llamadas con n ≥ 1 y
a[0] = 0 han de devolver b = true. Para saber por qué, seguir leyendo.

La técnica pre/post, debida a C.A.R. Hoare (1969), se basa en considerar que un
algoritmo es una función de estados en estados: comienza su ejecución en un estado
inicial válido descrito por el valor de los parámetros de entrada y, tras un cierto
tiempo cuya duración no es relevante a efectos de la especificación, termina en un
estado final en el que los parámetros de salida contienen los resultados esperados.

Si S representa la función a especificar, Q es un predicado que tiene como varia-
bles libres los parámetros de entrada de S, y R es un predicado que tiene como
variables libres los parámetros de entrada y de salida de S, la notación

{Q}S{R}

es la especificación formal de S y ha de leerse: “Si S comienza su ejecución en un
estado descrito por Q, S termina y lo hace en un estado descrito por R”.

Q recibe el nombre de precondición y caracteriza el conjunto de estados iniciales
para los que está garantizado que el algoritmo funciona correctamente. Describe las
obligaciones del usuario. Si este llama al algoritmo en un estado no definido por
Q, no es posible afirmar qué sucederá.

R recibe el nombre de postcondición y caracteriza la relación entre cada estado ini-
cial, supuesto este válido, y el estado final correspondiente. Describe las obligaciones
del implementador, supuesto que el usuario ha cumplido las suyas.









2. Predicados



Usaremos las letras mayúsculas P , Q, R, . . . , para denotar predicados de la lógica
de primer orden. La sintaxis se define inductivamente mediante las siguientes reglas:

1. Una expresión e de tipo bool es un predicado.

2. Si P es un predicado, ¬P , leído “no P ”, también lo es.

3. Si P y Q son predicados, P & Q también lo es, siendo & cualquiera de las
conectivas lógicas {∧, ∨, →, ↔}, leídas respectivamente “y”, “o”, “entonces”, “si y
solo si”.

Facultad de Informática - UCM

16

Capítulo 2. Especificación de algoritmos

4. Si P y Q son predicados, (∀w : Q(w) : P (w)) y (∃w : Q(w) : P (w)) también lo
son, denominados respectivamente cuantificación universal y cuantificación
existencial.

En lógica de primer orden, estas cuantificaciones se escriben con una sintaxis más sim-
ple (respectivamente ∀w . R(w) y ∃w . R(w), siendo R un predicado). La sintaxis edul-
corada propuesta aquí se escribiría entonces ∀w(Q(w)→P (w)) y ∃w(Q(w) ∧ P (w))
respectivamente. La hemos elegido porque facilitará la escritura de asertos sobre
programas.



Algunos ejemplos de predicados:

n ≥ 0
x > 0 ∧ x 6= y
0 ≤ i < n
∀w : 0 ≤ w < n : a[w] ≥ 0
∃w : 0 ≤ w < n : a[w] = x
∀w : 0 ≤ w < n : impar (w)→(∃u : u ≥ 0 : a[w] = 2u)

{abreviatura de 0 ≤ i ∧ i < n}

donde impar (x) es un predicado que determina si su argumento x es impar o no.



Es muy importante saber distinguir los dos tipos de variables que pueden aparecer
en un predicado:

Variables ligadas. Son las que están afectadas por un cuantificador, es decir, se
encuentran dentro de su ámbito. Por ejemplo, el ámbito del cuantificador en
(∀w : Q(w) : P (w)) son los predicados Q y P . Toda aparición de w en ellos que
no esté ligada a otro cuantificador más interno, está ligada al ∀w externo.

Variables libres. Son el resto de las variables que aparecen en el predicado. La
intención es que estas variables se refieran a variables o parámetros del algoritmo
que se está especificando.





En el predicado ∀w : 0 ≤ w < n : impar (w)→(∃u : u ≥ 0 : a[w] = 2u), las variables
n y a son libres, mientras que w y u son ligadas.

Una variable ligada se puede renombrar de forma consistente sin cambiar el signi-
ficado del predicado. Formalmente, si v no aparece en Q ni en P , entonces:

(∂ w : Q(w) : P (w)) ≡ (∂ v : Q(v) : P (v))

donde ∂ representa un cuantificador cualquiera (por ahora hemos presentado ∀ y ∃,
pero aparecerán más). Por ejemplo:

(∃w : 0 ≤ w < n : a[w] = x) ≡ (∃v : 0 ≤ v < n : a[v] = x)



Dado el uso tan diferente de las variables libres y ligadas y que el nombre de estas
últimas siempre se puede cambiar, utilizaremos en este curso la siguiente regla:

Las variables ligadas de un predicado nunca tendrán el mismo nombre
que una variable del programa que está siendo especificado o verificado.
Siempre que sea posible, usaremos las letras u, v, w, . . . para nombrar va-
riables ligadas.

Estructura de Datos y Algoritmos

3. Significado

17



Utilizaremos frecuentemente otras expresiones cuantificadas, de tipo entero en lu-
gar de booleano, que se han demostrado útiles en la escritura de predicados breves y
legibles. Son las siguientes (Q y P son predicados y e es una expresión entera):

P w : Q(w) : e(w)
suma de las e(w) tales que Q(w)
Q w : Q(w) : e(w)
producto de las e(w) tales que Q(w)
máx w : Q(w) : e(w) máximo de las e(w) tales que Q(w)
mín w : Q(w) : e(w) mínimo de las e(w) tales que Q(w)
# w : Q(w) : P (w)

número de veces que se cumple Q(w) ∧ P (w)

3. Sig
  • Links de descarga
http://lwp-l.com/pdf16258

Comentarios de: Capítulo 2 - Especificación de algoritmos (0)


No hay comentarios
 

Comentar...

Nombre
Correo (no se visualiza en la web)
Valoración
Comentarios
Es necesario revisar y aceptar las políticas de privacidad