Tal vez lo primero que debe hacerse a la hora de hacer una prueba de correctitud es entender qué hace el algoritmo y cómo lo hace. En este caso creo que está claro el "qué" y para el "cómo" es suficiente con hacer un seguimiento con algún ejemplo. Si no han dado este "primer paso", les recomiendo que lo hagan antes de continuar.
Una vez tengan una idea de cómo opera el algoritmo, puede abordarse el problema en dos fases: suponer, primero, que las líneas 3 a 9 corresponden a otro procedimiento (o función) y hacer una prueba de correctitud para tal procedimiento. Una vez hecho eso, puede probarse la correctitud del procedimiento completo teniendo en cuenta que se conoce cuál es la operación del ciclo interno y además que es correcta, suponiendo que las líneas 3 a 9 se reemplazan por una llamada (en una línea) a otra función, por lo tanto sólo interesa saber qué hace esa línea.
Consideren, por ejemplo, el ciclo interno: la operación de las líneas 6 a 8 puede resumirse diciendo intercambiar(A[j], A[j+1]), aunque sería necesario probar la correctitud de intercambiar(a, b). Y en el momento de hacer la prueba del ciclo completo, se considerarían dos casos: en uno, los valores de las posiciones j y j+1 se intercambian y en el otro no, sin necesidad de recorrer de nuevo el procedimiento intercambiar.
Un inconveniente a la hora de hacer las pruebas es la escritura de las proposiciones en forma matemática. La idea es que NO vamos a ser, por el momento, demasiado rigurosos, en cambio, utilizaremos un lenguaje mixto. Por ejemplo: es válido decir que, en algún punto de la ejecución del algoritmo, los elementos de las posiciones 1 a k, o si prefieren, el subarreglo A[1..k] contiene sólo números primos...
Espero que se genere discusión al respecto...
Suscribirse a:
Comentarios de la entrada (Atom)
8 comentarios:
Profe tengo una pregunta, despuès de probar la correctitud del ciclo interno y del intercambio , llegué a algo de la siguiente forma:
BubbleSort( A[1..n])
i <- length(A)
while(i>1)
ordenarParejasConsecutivas(1,i)
i <- i-1
end
El metodo ordenarParejasConsecutivas (1,i)ordena ascendentemente todas las parejas consecutivas desde el primer elemento hasta el i-èsimo. La pregunta es: en éste punto, ¿como serìa el invariante de ciclo? o ¿como se demuestra que el algoritmo anterior si ordena el arreglo?
...............
Respecto al comentario de Andrés...
La idea sería que en la prueba del ciclo externo, con el invariante adecuado, pueda usar de manera abstracta la operación del ciclo interior y la prueba sería algo como esto:
Paso Base => Para i = length[A] se tiene que [invariante de ciclo parametrizado con el valor length[A]] ya que [explicación].
Hipótesis de Inducción => Ahora supongamos que cuando i = k se tiene que [invariante de ciclo parametrizado con el valor k].
Paso Inductivo => Entonces, al ejecutar el ciclo, ordenarParejasConsecutivas(1, k) hace que [explicación], i toma el valor k - 1 y se tiene que [invariante de ciclo parametrizado con el valor k - 1] ya que [explicación].
Conclusión => El ciclo termina cuando i = [valor final], así que [invariante de ciclo parametrizado con el valor final] y por tanto el arreglo A[1..n] queda ordenando.
Ahora bien...me gustaría ver la forma en que probó la correctitud de ordenarParejasConsecutivas(1, i) porque no veo cómo pueda servirle para mostrar que Bubble-Sort ordene efectivamente el arreglo.
Nota: la expresión [explicación], la he usado para indicar que debe ir algún tipo de explicación, pero no quiere decir que sea la misma en cada punto. :D
Esta es una nota aclaratoria...
Uno de ustedes me escribió diciéndome que una idea que tenía para el invariante del ciclo interno era decir que "A[j] es mayor que los anteriores", o sea,
"A[j] >= A[j - 1],...., A[1]"
Sin embargo, esta proposición le causaba problemas a la hora de probar el caso base pues "para el
primer caso A[j - 1] es A[0] que no existe
por ende A[j] es mayor, pero como se escribió arriba no tiene sentido". No parece tener sentido porque se está comparando una cantidad inexistente con otra existente.
Para este tipo de situaciones, aclara un poco ver que puede formularse la misma porposición de la siguiente forma:
si X está en A[1..j - 1], entonces X <= A[j]
Así, para el primer caso se diría
si X está en A[1..0], entonces X <= A[1]
y esta proposición resultaría verdadera por la siguiente razón:
la proposición está escrita en la forma si p entonces q o p -> q si lo prefieren, donde:
p: X está en A[1..j - 1]
q: X <= A[j]
Para el caso base, p resulta falso ya que sin importar qué valor tenga X, éste no puede estar en A[1..0] ya que tal arreglo es vacío.
Ahora bien, si p es falso, sin importar el valor de verdad de q, la proposición p -> q es verdadera y por tanto la proposición es cierta para el caso base.
Advertencia: Una idea que también se discutió consistía en definir "que
cualquier elemento es mayor que vacío". Debe tenerse cuidado con las definiciones. En general, una definición asocia un símbolo con un concepto pero no atribuye propiedades a objetos.
Nótese que si puede decirse:
Definción: "cualquier elemento es mayor que vacio".
por qué no decir
Definción: "Bubble-Sort resuelve correctamente el problema de ordenamiento"
Dense cuenta de que estamos estudiando el "objeto" Bubble-Sort para decidir si resuelve correctamente o no el problema de ordenamiento, es decir, estamos tratando de encontrar una propiedad del algoritmo, en lugar de imponerla.
Así que para el caso del arreglo vacío, debería definirse qué es un arreglo vacío y de ahí concluir que cualquier elemento (número) es mayor que cualquier elemento del arreglo vacío.
Creo que al menos el primer punto tiene suficiente material para discutir, les invito a que aprovechen ;)
Gracias por su respuesta profesor. Respecto a su comentario, yo lo que hice fué probar la correctitud de las líneas 3 a 9 del algoritmo original (primero probé el intercambio y luego el ciclo interior) y las reemplacé por el método ordenarParejasConsecutivas. Es decir, ya sé y probé lo que hacen esas líneas y por eso las reemplacé por un método llamado ordenarParejasConsecutivas. Le envié a su correo lo que he hecho hasta el momento. Gracias por su tiempo y atención
Profe, tengo una duda, cómo puedo declarar el invariante para el ciclo interno como A[j] menor o mayor q otro elemento, si precisamente el ciclo invierte ese parámetro? Es decir, para probar la correctitud del ciclo interno, no se cómo puedo lograrlo con invariante si llego a declarar el mismo, ya que la prueba revisa antes y después de la ejecución del ciclo, gracias
Diego Franco
Respondiendo la inquietud de Diego...
Recuerde que el valor de verdad de la proposición que sirve como invariante de ciclo se evalúa al evaluar la condición del ciclo, es decir, si se tiene algo como
1. while([condición])
2. do...
3. ...
debe verificarse la veracidad de la invariante en la línea 1 sin importar qué pasa en las líneas 2 y 3. De hecho, al completar la prueba de correctitud, se asume que la invariante es verdera pero la condición del ciclo es falsa, de tal forma que puede decirse que al terminar el ciclo (condición falsa), se mantiene la invariante y el algoritmo es correcto.
De la misma forma, el paso base en la prueba de correctitud usando invariante, corresponde con la verificación de la veracidad de la invariante en la línea de la condición del ciclo antes de ejecutar por primera vez el cuerpo del ciclo.
Espero que esto ayude ;)
Respondiendo la inquietud de Damián, hay un
nuevo post...
Publicar un comentario