Escribiendo una prueba para un algoritmo

Question

Hola chicos, estoy tratando de comparar 2 algoritmos y pensé que podría intentar y escribir una prueba para ellos. (Mis matemáticas chupa así que por lo tanto, la pregunta)

Normalmente en nuestra lección de matemáticas del año pasado se nos daría una pregunta como

demostrar: (2r + 3) = n (n + 4)

entonces Haría las 4 etapas necesarias y obtendría la respuesta al final

Donde estoy atascado está probando prims y Kruskals - ¿cómo puedo obtener estos algoritmos en una forma como matemática anterior para poder proceder a probar

nota: no le estoy pidiendo a la gente wer para mí - sólo me ayudan a conseguir que en una forma donde puedo tener un ir yo mismo

gracias

Answer 1

Usted no da muchos detalles, pero hay una comunidad de matemáticos (Matemática Gestión del Conocimiento MKM) que han desarrollado herramientas para apoyar las pruebas de matemáticas en la computadora. Véase, por ejemplo:

http://imps.mcmaster.ca/

y la última conferencia de

http://www.orcca.on.ca/conferences/cicm09/mkm09/

Answer 2

De mis clases de matemáticas en Uni I (vagamente) recuerda que demuestra Prims y algoritmos Kruskals - y que no ataca escribiéndolo en forma matemática. En cambio, toma teorías comprobadas para Gráficos y las combina, p. Ej. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness para construir la prueba.

Si buscas probar la complejidad, simplemente por el funcionamiento del algoritmo es O (n^2). Hay algunas optimizaciones para el caso especial donde el gráfico es escaso y puede reducir esto a O (nlogn).

Answer 3

donde estoy atascado está demostrando prims y Kruskals - ¿Cómo puedo obtener estos algoritmos en una forma como la que se mathmatical anterior para que pueda proceder a probar

No creo que se pueda directamente. En cambio, demuestre que ambos generan un MST, luego demuestre que dos MST son iguales (o equivalentes, ya que puede tener más de un MST para algunos gráficos). Si ambos algoritmos generan MST que se muestran equivalentes, entonces los algoritmos son equivalentes.

Answer 4

Para demostrar la exactitud de un algoritmo, generalmente tiene que mostrar (a) que termina y (b) que su salida cumple con la especificación de lo que está tratando de hacer. Estas dos pruebas serán bastante diferentes de las pruebas algebraicas que mencionas en tu pregunta. El concepto clave que necesita es mathematical induction. (Es recursion para las pruebas.)

Tomemos como ejemplo quicksort.

Para demostrar que la clasificación rápida siempre termina, primero demostrar que termina de entrada de longitud 1. (Esta es trivialmente cierto.) A continuación, muestran que si termina de entrada de longitud hasta n, entonces se terminar para entrada de longitud n + 1. Gracias a la inducción, esto es suficiente para demostrar que el algoritmo termina para todas las entradas.

Para demostrar que el quicksort es correcto, debe convertir la especificación de la clasificación por comparación a un lenguaje matemático preciso. Queremos que la salida sea un permutation de la entrada de tal manera que si i ≤ j continuación un _i ≤ un _j. Demostrar que la salida de quicksort es una permutación de la entrada es fácil, ya que comienza con la entrada y simplemente intercambia elementos. Probar la segunda propiedad es un poco más complicado, pero de nuevo puedes usar la inducción.

Answer 5

La mayoría de las veces la prueba depende del problema que tenga en su mano. El argumento simple puede ser suficiente a veces, en otros momentos puede necesitar prueba rigurosa. Una vez usé un corolario y la prueba del teorema ya probado para justificar que mi algoritmo es correcto. Pero eso es para un proyecto universitario.

Answer 6

Quizás desee probar un método de prueba semiautomático. Solo para ir a algo diferente;) Por ejemplo, si tiene una especificación Java de los algoritmos de Prim y Kruskal, basándose óptimamente en el mismo modelo de gráfico, puede usar el KeY Prover para probar la equivalencia del algoritmo.

La parte crucial es formalizar su obligación de prueba en Dynamic Logic (esta es una extensión de lógica de primer orden con tipos y medios de ejecución simbólica de programas Java). La fórmula para demostrar podría coincidir con el (incompleta) siguiente patrón:

\forall Graph g. \exists Tree t. 
    (<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t) 

Esto expresa que para todos los gráficos, los dos algoritmos terminan y el resultado es el mismo árbol.

Si tiene suerte y su fórmula (y las implementaciones de algoritmo) son correctas, entonces KeY puede probarlo automáticamente. De lo contrario, es posible que necesite crear instancias de algunas variables cuantificadas, lo que hace que sea necesario inspeccionar el árbol de pruebas anterior.

Después de haber probado lo que sucede con KeY, puede estar contento de haber aprendido algo o intentar reconstruir una prueba manual de la prueba KeY: esto puede ser una tarea tediosa ya que KeY conoce muchas reglas específicas de Java que no son fáciles de comprender Sin embargo, tal vez pueda hacer algo como extraer una disyunción de Herbrand de los términos que KeY usó para crear instancias de cuantificadores existenciales en el lado derecho de los secuentes en la prueba.

Bueno, creo que la clave es una herramienta interesante y más gente debe acostumbrarse a probar el código Java crítica utilizando herramientas como eso;)