Supression de l'ancienne preuve de correction du renommage de variable globale : on utilise toujours la commutativité de Step mais plus du tout StarStep ni Forever.

Adaptation du renommage de variables globales pour utiliser le nouveau schema de simulation. On va pouvoir supprimer tout ce qui concerne star-step et forever.

Retour à la version exécutable du renommage de traces au lieu de la version relationnelle, pour pouvoir ensuite appliquer le résultat général sur la préservation de comportements.

[PROGRES] Preuve de préservation de comportement dans le cas où le comportement est modifié point à point par l'opération de refactoring (par exemple le renommage de variables globales).
Pour ce faire, et comme des traces infinies entrent en jeu, on utilise une fonction exécutable pour dénoter la relation entre les évènements issus de l'exécution du programme initial et ceux issus du programme transformé.

[FIX] J'avais construit une relation coinductive "Exists" sur les traces infinies, mais je m'apperçois que celle-ci ne fait pas ce que j'espérais. Elle n'était de toute façon pas utilisée. Donc je l'ai supprimée.

Utilisation des nouveaux résultats de RefactoringCorrectness.v. (Les anciens résultats, bien que plus généraux, sont devenus inutiles.)

Les paires de simulation identifiées dans RefactoringCorectness (Igor) sont un cas particulier des paires de simulationsidentifiées dans  AdditionalBehaviors.

Dans le cas où R_event est l'égalité, le fsim_properties d'Igor est un cas particulier du schema de simulation lockstep sans preservation de l'interface. (Et on pourra donc exploiter des résultats sur ce schema au lieu de les re-démontrer).

+ Remodularisation, et reorganisation des dépendances.

[CLEAN] Supression de résultats devenus inutiles (on a utilisé le concept de lock-step simulation introduit plus tôt).

Utilisation du principe de lockstep-simulation pour prouver la preservation de comportement sur le renommage local de label. On part de la commututativité de [step] déjà établie et on utilise directement les outils de AdditionalSmallstep et AdditionalBehaviors au lieu de passer par les anciens résultats sur StarStep, NoStep, Forever etc.

Reformulation du résultat de commutativité de step pour mieux coller à la façon dont ces résultats sont attendus dans compcert.Smallstep et refaccert.AdditionalSmallstep.

Quand on a une paire de lock-step simulations, on a une bisimulation stricte pour les comportements.

Résultats concernant la préservation des cas d'erreur lorsqu'on a une paire de lock-step simulations.

Modification d'énoncés pour souligner que c'est la préservation FW de la non-finalité des états et la préservation de non-existance d'états initiaux qui compte. e fait que ça revienne à une préservation BW de la finalité ou initilité des états sera intéressant dans un deuxième temps.

Nouveau résultat qui renforce un résultat de préservation de comportement de Compcert dans le cas ou on a une préservation de nostep.

Preuve de forward_simulation (concept de Compcert/common/Smallstep.v) en utilisant step_commut (de rename_loclabel) et sans untiler star_step etc.

Nouveau résultat pour faire le lien entre nos STEP_COMMUT qui utilisent une pécondition et lock-step fw-simulation de Smallstep.v de Compcert.

Tentative de remplacer les fonctions de transformations d'évènements/traces par des relations. On se retrouve bloqué sur les traces infinies pour montrer l'existence d'une trace transformée lorsque celle-ci est infinie. On utilise finalement une fonction exécutable pour montrer l'existence, et donc on a côte à côte les deux versions : la relation et la fonction. Pas sûr qu'on ait vraiement gagné quelque chose.