GitLab

Précondition nécessaire sur les transformations de programmes (et dans le commit précédent pour les transforations intermédiaires).

[REFACTORING] Déplacement de modules dans de nouveau répertoires pour hiérarchiser les modules "communs" selon Syntaxe/Sémantique générale (évènements, environnements) /Sémantique Csem.

[REFACTORING] Resolution de la complexite pour NoStep. En reprenant le fait que les états que l'on considère sont atteugnables, on s'appuie sur des propriétés invariantes, et ça simplifie le problème.

[REFACTORING] Supression du la précondition nécessaire sur les environnements globaux car son utilisation rendait le schéma géréral de la preuve moins clair (pour no-step et star-step).

Déduction de STAR_STEP_COMMUT depuis STEP_COMMUT. CEla nécessite d'avoir une précondition suffisante stable (et aussi la transformation d'états doit être fonctionnelle (une fonction, déterministe).

Ceci va nous permettre de factoriser cette partie du code un peu pénible dans plusieurs transformations, et aussi de mieux expliquer ce qu'on doit prouver en amont pour avoir la bisimulation (la précondition suffisante stable en particulier).

[REFACTORING] Clarification du rôle de la non-apparition dans l'environnement global (en donnant un nom expliquant le role, qui est de garantir la preservation de la non apparition).

[REFACTORING] Explicitation d'une précondition de plusieurs lemmes car l'apparition de son nom (N_PRE pour necessary_precondition) laissait penser qu'elle était utilisé pour son caractère nécessaire, alors qu'elle était utilisée dans ses lemmes de manière suffisante.

+ [REFACTORING]