Pregunta sobre la prueba formal del recorrido Inorder

Question

En la famosa serie de libros de Don Knuth, El arte de la programación de computadoras, Sección 2.3.1, describe un algoritmo para atravesar el árbol binario en orden, haciendo uso de una pila auxiliar:

T1 Initialize.] Establezca pila $ rm a $ vacía y establezca la variable de enlace $ rm p obtiene t $

T2 $ rm p = lambda $?] Si $ rm p = lambda $, vaya al paso t4.

T3 Stack $ rm ; Leftarrow P $] (ahora $ rm P $ apunta a un árbol binario no vacío que se va a atravesar). Pulse el valor de $ rm P $ en la pila $ rm a $, luego, luego establecer $ rm p gets llink (p) $

T4 $ rm P LeftRarw Stack $] Si la pila $ rm a $ está vacía, el algoritmo termina; de lo contrario, haga la parte superior de $ rm a $ a $ rm P $.

T5 Visite $ rm P $] Visite $ rm nodo (p) $. Luego establezca $ rm P obtiene rlink (p) $ y regrese al paso T2.

Podemos trazar un diagrama de flujo del algoritmo. En el párrafo siguiente, le da un prueba formal del algoritmo:

Comenzando en el paso T2 con $ rm P $ A puntero a un árbol binario de $ n $ nodos y con la pila $ rm a $ que contiene $ rm a [1] dotsc a [m] $ por unos $ m Ge 0 $, el procedimiento de los pasos T2-T5 atravesará el árbol binario en cuestión, en orden, y luego llegará al paso T4 con pila $ rm a $ devuelto a su valor original $ rm a [1] dotsc A [m] $.

Sin embargo, hasta donde yo sé, una prueba formal es bastante diferente del método general descrito en la Sección 1.2.1:

Para cada cuadro en el diagrama de flujo, que si una afirmación adjunta a cualquier flecha que conduce a la caja es verdadera antes de que se realice la operación en ese cuadro, entonces todas las afirmaciones de flechas relevantes que se alejan de la caja son verdaderas después de la operación.

De hecho, dicho método es algo equivalente a Lógica de Hoare, que se utiliza para verificar formalmente la validez de los algoritmos.

¿Podemos convertir la declaración mencionada para probar el algoritmo de recorrido en un esquema de lógica de Hoare, o el alcance de afirmación de un diagrama de flujo?

¡Gracias!

Answer 1

Definitivamente es posible analizar este algoritmo usando Hoare Triples. El primer paso sería reemplazar las llamadas del procedimiento de visita con un mecanismo de contabilidad más razonable, digamos una lista que enumera los nodos visitados en orden. Luego define formalmente qué es un árbol binario y qué es un traversal de orden, algo a lo largo de las siguientes líneas:

Tree = Leaf N | Node N LTree RTree
Inorder(Leaf N) = N
Inorder(Node N LTree RTree) = Inorder(LTree) || N || Inorder(RTree)

Aquí n está el "nombre" del nodo, y || es la concatenación de la lista. Armado con estas nociones, es un ejercicio construir los triples Hoare requeridos. Probablemente necesitará encontrar aún más nociones (por ejemplo, deberá explicar cuáles son los contenidos de la pila cuando aparece un nodo P).

¿Qué ganamos de este ejercicio? ¿Entendemos mejor el algoritmo? Probablemente no. Pero entendemos cómo razonar con precisión sobre los algoritmos, algo que es útil si planea hacer verificación de software o teoría del lenguaje de programación, áreas que forman la llamada "teoría B". Si eres más un tipo de "teoría" (algoritmos y complejidad), entonces, como yo, encontrarás tales ejercicios por el caso.