Estrategias generales de prueba para mostrar la corrección de las funciones recursivas?

Question

Me pregunto si existe alguna regla/esquema de proceder con la corrección del algoritmo de prueba? Por ejemplo, tenemos una función $ F $ definido en los números naturales y se define a continuación:

function F(n,k) 
begin 
    if k=0 then return 1 
    else if (n mod 2 = 0) and (k mod 2 = 1) then return 0 
    else return F(n div 2, k div 2); 
end; 

donde $ n \ \ text {div} \ 2 = \ left \ lfloor \ frac {n} {2} \ right \ rfloor $

la tarea es demostrar que $ F (n, k) = \ begin {cases} 1 \ Leftrightarrow {n \ choose k} \ \ text {mod} \ 2 = 1 \ 0 \ text {else} \ end {cases} $

No parece muy complicado (¿estoy equivocado?), pero no sé cómo se debe estructurar este tipo de pruebas. Estaría muy agradecido por la ayuda.

Answer 1

La corrección de los algoritmos recursivos a menudo se prueba en mathematical induction. Este método consta de dos partes: primero, establece la base y luego utiliza un paso inductivo.

En su caso, la base es todos los casos cuando k = 0, o cuando k es impar pero n es par.

El paso inductivo requiere demostrando que cuando f(n,k) es correcta, f(2*n,2*k), f(2*n+1,2*k), y f(2*n,2*k+1)f(2*n+1,2*k+1) son los correctos.

Answer 2

En general, se intentará una prueba por inducción para mostrar la corrección. Esto funciona muy bien cuando se prueba la corrección de las funciones recursivas, ya que puede probar el caso base directamente, y luego puede usar el hecho de que la función funciona para entradas "más pequeñas" para demostrar que funciona para la siguiente entrada más grande.

En este caso, intentaré una prueba por inducción bien fundamentada. Específicamente, probaría que

1. La función es correcta para todas las entradas de la forma (n, 0).
2. Suponiendo que para todas las entradas (n ', k') tal que (n ', k') es lexicográficamente menor que (n, k), la función es correcta, compruebe que es correcta para (n, k) .

Las especificaciones de esta prueba necesitarían aprovechar las características específicas de su función y el bahvaior de los coeficientes binomiales, pero la plantilla general es la anterior.

Espero que esto ayude!

Answer 3

Fuera de demostrar su lógica matemáticamente (ejemplo: inductive proof), existen algunos resultados en la ciencia de la informática relacionados con esto.

Puede comenzar aquí para ver un esquema del sujeto: Correctness
para su caso particular, que estaría interesado en la corrección parcial para mostrar que la respuesta es la prevista. Entonces la corrección total para mostrar que el programa termina.

Hoare logic puede resolver su corrección parcial.

En cuanto a la terminación de este problema en particular:

Si (n% 2 == 0 y k% 1 == 1) o (k == 0) el programa termina, de lo contrario recursivamente a la n/2, k/2 caso.
Utilizando strong induction en k, podemos demostrar que el programa siempre llega a uno de los nodos de terminal donde k == 0. (Puede terminar antes en la primera cláusula, pero solo necesitamos mostrar que termina, lo que sí ocurre)

Así que dejé la prueba de corrección parcial para usted (porque no sé eso)