Question sur la preuve formelle de la traversée infixe

Question

célèbre série de livres de Don Knuth, L'art de la programmation informatique , la section 2.3.1, il décrit un algorithme pour parcourir arbre binaire en afinde, en utilisant une pile auxiliaire:

T1 [Initialiser.] Set pile $ \ rm A $ vider et définir la variable de liaison $ \ rm P \ obtient T $

T2 [$ \ rm P = \ Lambda $?] Si $ \ rm P = \ Lambda $, aller à T4 étape.

T3 [Stack $ \ rm \; \ Leftarrow P $] (. Maintenant $ \ rm P points de $ à un arbre binaire non vide qui doit être déplacé) pousser la valeur de $ \ rm P $ sur pile $ \ rm A $, puis régler $ \ rm P \ obtient Llink (P) $

T4 [$ \ rm P \ Leftarrow Stack $] Si la pile $ \ rm $ est vide, l'algorithme se termine; sinon pop haut de $ \ rm $ à $ \ rm P $.

T5 [Visitez $ \ rm P $] Visitez $ \ rm NODE (P) $. Réglez ensuite $ \ rm P \ obtient RLINK (P) $ et retour à l'étape T2.

Nous pouvons tracer un organigramme de l'algorithme. Dans le paragraphe suivant, il donne une la preuve formelle de l'algorithme:

À partir de l'étape T2 avec $ \ rm P $ un pointeur sur un arbre binaire de noeuds $ n $ et avec la pile $ \ rm A $ contenant $ \ rm A [1] \ dotsc A [m] $ pour certaines $ m \ ge 0 $, la procédure des étapes T2-T5 va traverser l'arbre binaire en question, afinde, et ensuite arriver à T4 étape avec pile $ \ rm A $ revenue à sa valeur d'origine $ \ rm A [1 ] \ dotsc A [m] $.

Cependant, pour autant que je sache, une telle preuve formelle est tout à fait différente de la méthode générale décrite dans la section 1.2.1:

pour chaque zone dans le diagramme d'écoulement, que, si une assertion ci-joint une quelconque flèche débouchant dans la boîte est vrai avant l'opération en ce que la boîte est réalisée, alors toutes les affirmations sur les flèches appropriées menant à une distance de la boîte sont remplies après l'opération.

En fait, une telle méthode est un peu l'équivalent Hoare , qui est utilisé pour vérifier formellement la validité des algorithmes .

Peut-on tourner la déclaration mentionnée pour prouver l'algorithme de déplacement dans un schéma de la logique de Hoare, ou l'affirmation-fixation d'un organigramme?

Merci!

Answer 1

Il est certainement possible d'analyser cet algorithme en utilisant triplets Hoare. La première étape serait de remplacer les appels de procédure de visite avec un mécanisme comptable plus raisonnable, par exemple une liste qui répertorie les noeuds visités dans l'ordre. Vous définissez ensuite formellement ce qu'est un arbre binaire est et ce qu'est un parcours infixe est quelque chose le long des lignes suivantes:

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

Ici N est le « nom » du nœud, et || est la concaténation de liste. Armé de ces notions, il est un exercice pour construire les triplets Hoare nécessaires. Vous aurez probablement besoin de trouver des notions encore plus (par exemple, vous aurez besoin d'expliquer ce que le contenu de la pile sont quand un nœud est sauté P).

Que gagnons-nous de cet exercice? Est-ce que nous comprenons l'algorithme mieux? Probablement pas. Mais nous comprenons comment raisonner précisément sur les algorithmes, ce qui est utile si vous prévoyez de faire la vérification du logiciel ou la programmation théorie des langages, des zones formant le soi-disant « Théorie B ». Si vous êtes plus d'un type « Théorie A » (algorithmes et complexité) puis, comme moi, vous trouverez ces exercices un peu à côté du point.