1. 04 Jul, 2022 3 commits
  2. 30 Jun, 2022 2 commits
  3. 28 Jun, 2022 3 commits
  4. 27 Jun, 2022 1 commit
    • Julien COHEN's avatar
      [PROGRES] Preuve de préservation de comportement dans le cas où le... · 726f1bac
      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.
      726f1bac
  5. 20 Jun, 2022 4 commits
  6. 17 Jun, 2022 1 commit
  7. 15 Jun, 2022 1 commit
  8. 14 Jun, 2022 3 commits
  9. 13 Jun, 2022 1 commit
  10. 10 Jun, 2022 3 commits
  11. 07 Jun, 2022 5 commits
  12. 03 Jun, 2022 1 commit
    • Julien COHEN's avatar
      Utilisation du principe de lockstep-simulation pour prouver la preservation de... · 0785044f
      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.
      0785044f
  13. 24 May, 2022 2 commits
  14. 19 May, 2022 2 commits
  15. 17 May, 2022 2 commits
  16. 16 May, 2022 1 commit
  17. 13 May, 2022 1 commit
  18. 28 Apr, 2022 3 commits
  19. 12 Apr, 2022 1 commit
    • Julien COHEN's avatar
      Tentative de remplacer les fonctions de transformations d'évènements/traces... · 477b4c5b
      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.
      477b4c5b