Solución del problema 35

 

35. Se desea crear una función cuyo objetivo sea realizar una búsqueda binaria de un valor, x, sobre el vector ordenado v para encontrar la primera posición del vector ocupada por un valor mayor que x.

  • Escribir la precondición y postcondición que deberían cumplirse. Escribir la cabecera y las cláusulas require y ensure de una función Eiffel que implementara esa función.
  • De acuerdo con la precondición y postcondición anteriores, desarrollar una batería de pruebas para esa función mediante el método de caja negra.
  • Verificar la corrección total de las siguientes implementaciones de esta función:
const N = ..;

function busq1(v: array[1..N] of real; x: real) dev p: integer;
var
izda,dcha,med: integer;
begin
{ N ≥ 0, α : 1 ≤ α < N : vα ≤ vα+1 }
<izda,dcha> := <1,N>;
while izda <= dcha do
begin
med := (izda+dcha) div 2;
if v[med] < x then izda := med+1 else dcha := med-1;
end;
p := izda
end;

function busq2(v: array[1..N] of real; x: real) dev p: integer;
var
izda,dcha,med: integer;
begin
{ N ≥ 0, α : 1 ≤ α < N : vα ≤ vα+1 }
<izda,dcha> := <1,N>;
while izda < dcha do
begin
med := (izda+dcha) div 2;
if v[med] < x then izda := med else dcha := med;
end;
p := dcha+1
end;
 

La precondición debe exigir que el vector esté ordenado. Se puede incluir la condición de que N sea mayor que cero (es decir, que el vector contenga al menos un elemento) o bien omitirla permitiendo que se pueda buscar en un vector vacío (permitido en Eiffel). Nosotros vamos a imponer la existencia de al menos un elemento porque así la verificación es un poco más sencilla. La postcondición debe expresar exactamente el significado del resultado. En éste caso el resultado p debe ser la posición del primer valor del array mayor que x. Esto significa que vp debe ser mayor que x y vp-1 debe ser menor o igual que x. Existen casos especiales cuando todos los elementos del vector son mayores que x o menores/iguales que x, ya que o bien p o p-1 apuntan fuera de los límites del array. Podeis ver estos casos en los gráficos siguientes, junto con la precondición y postcondición:

La cabecera de la función en Eiffel podría escribirse así: (Nota: La comprobación de si el array está ordenado no se puede hacer directamente en la cláusula require, por lo que se realiza utilizando una función adicional).

busq(v: ARRAY[REAL]; x: REAL) : INTEGER is
require
(v.lower = 1) and (v.count > 0) and then ordenado(v);
local
do
ensure
(1 <= Result) and (Result <= v.count+1);
((2 <= Result) and (Result <= v.count)) implies ((v.item(Result-1) <= x) and (x < v.item(Result)));
(1 = Result) implies (x < v.item(1));
(Result = v.count+1) implies (v.item(v.count) <= x);
end -- busq

ordenado(v: ARRAY[REAL]) : BOOLEAN is
local
i : INTEGER;
do
from i := v.lower;
until (i >= v.upper) or else (v.item(i) > v.item(i+1)) loop
i := i+1
end
Result := i >= v.upper
end -- ordenado

Las clases de equivalencia se obtienen directamente de la precondición (de su negación, ya que el objetivo es verificar si se detecta o no un fallo de precondición) y la postcondición (recordar que las clases deben expresar condiciones sobre las entradas, no sobre los resultados):

La clase 1.1 la hemos escrito como { N = 0 } en lugar de { N ≤ 0 } porque no tiene sentido un tamaño negativo del array. La clase 1.2 la podríamos haber escrito de manera más formal, pero no es imprescindible ya que el enunciado carece de ambiguedad. Por último, recordar que en las clases derivadas de la postcondición se asume implicitamente el cumplimiento de la precondición (vector no vacío y ordenado).
Una posible batería de pruebas podría ser la siguiente (los valores límite se muestran en rojo, y se muestra la condición que ha motivado su inclusión):

No hemos añadido valores límite para las relaciones "mayor que" entre x y los elementos del vector porque estamos tratando con números reales.

Verificación parcial. Reescribimos el algoritmo indicando los puntos de verificación. Para que las fórmulas sean menos farragosas voy a acortar los nombres de las variables:

function busq1(v: array[1..N] of real; x: real) dev p: integer;
var
i,d,m: integer;
begin
{ N > 0, α : 1 ≤ α < N : vα ≤ vα+1 }
<i,d> := <1,N>;
(1)-0
while i <= d do
begin
(2)-n
m := (i+d) div 2;
(3)-n
if v[m] < x then
begin
(4a)-n
i := m+1
(5a)-n
end else begin
(4b)-n
d := m-1
(5b)-n
end
(1)-n
end;
(6)
p := i
(7)
end;

La verificación de este código es un poco complicada, es necesario ayudarse con una comprensión de como trabaja este algoritmo. En primer lugar, si nos fijamos en como cambian i y d dentro del bucle (ver gráfico siguiente) podemos apreciar que en el punto invariante la parte del vector a la izquierda de i es menor o igual que x y la parte del vector a la derecha de d es mayor que x. Hay que tener cuidado porque no está garantizado que i y d se encuentren siempre dentro de los límites del vector.

Por otra parte, al terminar el bucle es necesario que i y d sean contiguos, porque en caso contrario existiría un solapamiento de zonas en el vector a la vez mayores y menores/iguales que x:

Por último, en el punto (3)-n es necesario que podamos garantizar que el acceso al vector se realiza dentro del rango adecuado. Por lo tanto en ese punto se debe cumplir 1 ≤ m ≤ N. Si juntamos estas condiciones en un candidato a invariante y observamos la postcondición que se obtiene:

Obtenemos una postcondición "parecida" a la requerida. Sin embargo, nos falta garantizar que p se encuentra dentro de los límites 1 ≤ p ≤ N+1. Si imponemos esta condición, mediante derivación inversa llegamos a que se debe cumplir en el invariante que 1 ≤ i ≤ N+1 y 0 ≤ d ≤ N. Iteramos el nuevo candidato a invariante:

Vemos que el invariante se mantiene constante. Veamos si la precondición del bucle implica al invariante:

Nota: Recordad que una condición del tipo (falso => lo que sea) vale cierto. Fijaros en que sólo se exige a N que sea mayor o igual que cero, por lo que podríamos sustituir en la precondición { N > 0 } por { N ≥ 0 } sin problemas.
Por último vamos a ver cual sería la postcondición:

La postcondición no coincide con la deseada. De hecho, ésta función calcula la posición del primer elemento mayor o igual a x. En realidad, mi propósito cuando escribí este problema era dar una función que sí cumpliera la postcondición, pero me equivoqué en la comparación de v[m] con x. Os lo comento para que veais que es muy fácil equivocarse y por eso el conocer las técnicas de verificación es algo imprescidible si queremos estar seguros de que nuestro código hace la tarea que deseamos.

CESAR VACA RODRIGUEZ
cvaca@infor.uva.es