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...
