- 04 Jul, 2022 3 commits
-
-
Julien COHEN authored
-
Julien COHEN authored
-
Julien COHEN authored
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.
-
- 30 Jun, 2022 2 commits
-
-
Julien COHEN authored
-
Julien COHEN authored
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.
-
- 28 Jun, 2022 3 commits
-
-
Julien COHEN authored
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.
-
Julien COHEN authored
-
Julien COHEN authored
-
- 27 Jun, 2022 1 commit
-
-
Julien COHEN authored
[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.
-
- 20 Jun, 2022 4 commits
-
-
Julien COHEN authored
-
Julien COHEN authored
-
Julien COHEN authored
-
Julien COHEN authored
-
- 17 Jun, 2022 1 commit
-
-
Julien COHEN authored
Utilisation des nouveaux résultats de RefactoringCorrectness.v. (Les anciens résultats, bien que plus généraux, sont devenus inutiles.)
-
- 15 Jun, 2022 1 commit
-
-
Julien COHEN authored
-
- 14 Jun, 2022 3 commits
-
-
Julien COHEN authored
Les paires de simulation identifiées dans RefactoringCorectness (Igor) sont un cas particulier des paires de simulationsidentifiées dans AdditionalBehaviors.
-
Julien COHEN authored
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).
-
Julien COHEN authored
-
- 13 Jun, 2022 1 commit
-
-
Julien COHEN authored
+ Remodularisation, et reorganisation des dépendances.
-
- 10 Jun, 2022 3 commits
-
-
Julien COHEN authored
-
Julien COHEN authored
-
Julien COHEN authored
-
- 07 Jun, 2022 5 commits
-
-
Julien COHEN authored
-
Julien COHEN authored
-
Julien COHEN authored
-
Julien COHEN authored
[CLEAN] Supression de résultats devenus inutiles (on a utilisé le concept de lock-step simulation introduit plus tôt).
-
Julien COHEN authored
-
- 03 Jun, 2022 1 commit
-
-
Julien COHEN authored
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.
-
- 24 May, 2022 2 commits
-
-
Julien COHEN authored
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.
-
Julien COHEN authored
-
- 19 May, 2022 2 commits
-
-
Julien COHEN authored
Quand on a une paire de lock-step simulations, on a une bisimulation stricte pour les comportements.
-
Julien COHEN authored
-
- 17 May, 2022 2 commits
-
-
Julien COHEN authored
Résultats concernant la préservation des cas d'erreur lorsqu'on a une paire de lock-step simulations.
-
Julien COHEN authored
-
- 16 May, 2022 1 commit
-
-
Julien COHEN authored
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.
-
- 13 May, 2022 1 commit
-
-
Julien COHEN authored
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.
-
- 28 Apr, 2022 3 commits
-
-
Julien COHEN authored
-
Julien COHEN authored
Preuve de forward_simulation (concept de Compcert/common/Smallstep.v) en utilisant step_commut (de rename_loclabel) et sans untiler star_step etc.
-
Julien COHEN authored
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.
-
- 12 Apr, 2022 1 commit
-
-
Julien COHEN authored
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.
-