Begin redaction of README.

2 files changed, 1560 insertions, 0 deletions

diff --git a/readme.pdf b/readme.pdf
new file mode 100644
index 0000000..a0d4280
--- /dev/null
+++ b/readme.pdf
diff --git a/readme.tm b/readme.tm
new file mode 100644
index 0000000..2f0e33f
--- /dev/null
+++ b/readme.tm
@@ -0,0 +1,1560 @@
+<TeXmacs|1.0.7.18>
+
+<style|article>
+
+<\body>
+  <doc-data|<doc-title|scade-analyzer>|<doc-subtitle|note de référence>>
+
+  <section|Introduction>
+
+  Le projet consiste en la réalisation d'un analyseur statique pour des
+  programmes SCADE, utilisant l'interprétation abstraite comme base de
+  travail. Les objectifs attendus sont :
+
+  <\itemize>
+    <item>Preuve de propriétés de sûreté sur des programmes
+
+    <item>Étude d'intervalles de variation pour des variables
+  </itemize>
+
+  L'expérience a été menée sur un sous-ensemble très restreint du langage
+  SCADE, comportant notamment :
+
+  <\itemize>
+    <item>noyau dataflow (opérations arithmétiques élémentaires, opérateurs
+    <verbatim|-\<gtr\>> et <verbatim|pre>), pas de prise en charge des
+    horloges explicites (primitves <verbatim|when>, <verbatim|merge>, ...)
+
+    <item>blocs <verbatim|activate>
+
+    <item>automates simples, à transitions faibles seulement, sans actions
+    sur les transitions (les transitions de type <verbatim|restart> sont
+    prises en compte)
+  </itemize>
+
+  Dans ce document nous metterons au clair les points suivants :
+
+  <\enumerate>
+    <item>Spécification du sous-ensemble de SCADE considéré
+
+    <item>Explication du fonctionnement de l'interprète pour la sémantique
+    concrète
+
+    <item>Explication de la traduction d'un programme SCADE en une formule
+    logique représentant le cycle du programme
+
+    <item>Explications sur l'interprétation abstraite en général, sur les
+    domaines numériques, sur la recherche de points fixe
+
+    <item>Explications sur notre adaptation de ces principes à l'analyse du
+    langage SCADE, en particulier :
+
+    <\itemize>
+      <item>itérations chaotiques
+
+      <item>domaines capables de faire des disjonctions de cas (graphes de
+      décision)
+    </itemize>
+  </enumerate>
+
+  <section|Spécification>
+
+  <subsection|Grammaire>
+
+  <\verbatim-code>
+    <\verbatim>
+      decl \ \ \ := CONST id: type = expr;
+
+      \ \ \ \ \ \ \ \ \ \| NODE (var_def;*) RETURNS (var_def;*) VAR var_def;*
+      body
+
+      var_def := (PROBE? id),* : type
+
+      body \ \ \ := LET eqn;* TEL
+
+      \ \ \ \ \ \ \ \ \ \| eqn;
+
+      type \ \ \ := INT \| BOOL \| REAL \| (TYPE,+)
+
+      eqn \ \ \ \ := id = expr
+
+      \ \ \ \ \ \ \ \ \ \| GUARANTEE id : expr
+
+      \ \ \ \ \ \ \ \ \ \| ASSUME id : expr
+
+      \ \ \ \ \ \ \ \ \ \| AUTOMATON state* RETURNS id,*
+
+      \ \ \ \ \ \ \ \ \ \| ACTIVATE scope_if RETURNS id,*
+
+      scope_if := (VAR var_def;*)? body
+
+      \ \ \ \ \ \ \ \ \ \| IF expr THEN scope_if ELSE scope_if
+
+      state \ \ \ := INITIAL? STATE id
+
+      \ \ \ \ \ \ \ \ \ \ \ \ \ body
+
+      \ \ \ \ \ \ \ \ \ \ \ \ \ until*
+
+      until \ \ \ := UNTIL IF expr (RESUME\|RESTART) id
+
+      expr \ \ \ \ := int_const \| real_const \| TRUE \| FALSE \| id
+
+      \ \ \ \ \ \ \ \ \ \ \| unary_op expr \| expr bin_op expr
+
+      \ \ \ \ \ \ \ \ \ \ \| IF expr THEN expr ELSE expr
+
+      \ \ \ \ \ \ \ \ \ \ \| id ( expr,* )
+
+      unary_op := - \| PRE \| NOT
+
+      bin_op \ \ := + \| - \| * \| / \| -\<gtr\> \| AND \| OR \| MOD
+    </verbatim>
+
+    \ \ \ \ \ \ \ \ \ \ \| = \| \<less\>\<gtr\> \| \<less\> \| \<gtr\> \|
+    \<less\>= \| \<gtr\>=
+  </verbatim-code>
+
+  <subsection|Sémantique concrète>
+
+  Pour simplifier, on considère dans cette section que tous les noeuds ont
+  été inlinés.
+
+  On note <math|\<bbb-X\>> l'ensemble des variables définies dans le texte du
+  programme, et on note <math|\<bbb-V\>> l'ensemble des valeurs qui peuvent
+  être prises.
+
+  Un environnement de valeurs est une fonction
+  <math|s:\<bbb-X\>\<rightarrow\>\<bbb-V\>> qui décrit un état de la mémoire
+  du programme. On définit aussi un sous-ensemble
+  <math|\<bbb-V\><rsub|i>\<subset\>\<bbb-V\>> de variables dont les valeurs
+  sont des entrées du système.
+
+  L'exécution d'un programme est une séquence d'états mémoire
+  <math|s<rsub|0>\<nocomma\>,s<rsub|1>,\<ldots\>,s<rsub|n>,\<ldots\>>
+  conforme à la spécification du programme et à une série d'entrées. On note
+  :
+
+  <\equation*>
+    s<rsub|0><long-arrow|\<rubber-rightarrow\>|i<rsub|1>>s<rsub|1><long-arrow|\<rubber-rightarrow\>|i<rsub|2>>s<rsub|2>\<rightarrow\>\<cdots\>
+  </equation*>
+
+  Dans la sémantique par traduction, la sémantique d'un programme est définie
+  par traduction du programme <math|P> en une formule logique <math|F> telle
+  que :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s<rsub|n-1><long-arrow|\<rubber-rightarrow\>|i<rsub|n>>s<rsub|n>>|<cell|\<Leftrightarrow\>>|<cell|<choice|<tformat|<table|<row|<cell|\<forall\>x\<in\>\<bbb-V\><rsub|i>,s<rsub|n><around*|(|x|)>=i<rsub|n><around*|(|x|)>>>|<row|<cell|F<around*|(|s<rsub|n-1>,s<rsub|n>|)>>>>>>>>>>
+  </eqnarray*>
+
+  Dans la sémantique par réduction, la sémantique d'un programme est définie
+  par un ensemble de règles de réduction qui aboutissent à
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s<rsub|n-1><long-arrow|\<rubber-rightarrow\>|i<rsub|n>>s<rsub|n>>|<cell|\<Leftrightarrow\>>|<cell|<frac|s<rsub|n-1>\<Rightarrow\>i<rsub|n>|s<rsub|n-1>\<Rightarrow\>s<rsub|n>>>>>>
+  </eqnarray*>
+
+  Pour un programme bien typé, étant donné <math|s<rsub|n-1>> et
+  <math|i<rsub|n>>, il existe un unique état <math|s<rsub|n>> qui remplit la
+  condition.
+
+  Pour traduire l'init et le reset, on introduit dans chaque scope
+  <math|\<Sigma\>> plusieurs variables :
+
+  <\itemize>
+    <item><math|nreset<rsub|\<Sigma\>>> : indique que le scope devra être
+    reset lors du prochain cycle
+
+    <item><math|init<rsub|\<Sigma\>>> : indique que le scope est à l'état
+    initial dans ce cycle
+
+    <item><math|active<rsub|\<Sigma\>>> : indique qu'un scope est actif dans
+    ce cycle
+  </itemize>
+
+  Un nouveau scope est introduit dans chaque body d'un bloc activate ou d'un
+  état d'automate.
+
+  De même, les automates introduisent deux variables :\ 
+
+  <\itemize>
+    <item><math|state<rsub|A>>, qui définit l'état de l'automate à ce cycle
+
+    <item><math|nstate<rsub|A>>, qui définit l'état de l'automate au cycle
+    suivant, en supposant qu'il n'y a pas de reset du scope où l'automate est
+    défini
+  </itemize>
+
+  L'état <math|s<rsub|0>> est défini par <math|s<rsub|0><around*|(|reset<rsub|/>|)>=true>,
+  où <math|/> est le scope racine englobant tout le programme ; toutes les
+  autres variables de <math|\<bbb-V\>> pouvant prendre n'importe quelle
+  valeur.
+
+  On suppose que chaque instance de <verbatim|pre> est numérotée, et pour
+  chaque <math|pre<rsub|i> e>, on introduit la variable <math|m<rsub|i>> qui
+  enregistre la valeur de <math|e> dans l'état et qui sert de mémoire pour le
+  pre.
+
+  Par la suite, que ce soit dans l'étude de la sémantique par réduction ou
+  par traduction, on notera toujours <math|l> la mémoire (c'est-à-dire
+  <math|s<rsub|n-1>>) et <math|s> l'état courant (c'est-à-dire
+  <math|s<rsub|n>>, sur lequel on travaille).
+
+  <subsection|Sémantique par réduction>
+
+  On définit notre ensemble d'environnements comme étant
+  <math|\<bbb-X\>\<rightarrow\>\<bbb-V\>\<cup\><around*|{|\<top\>|}>>, la
+  valeur <math|\<top\>> signifiant qu'une variable n'a pas encore pris sa
+  valeur.
+
+  Pour chaque élément de programme, on va introduire un certain nombre de
+  règles de réduction. On applique ces règles jusqu'à en déduire
+  <math|l\<Rightarrow\>s>, avec <math|\<forall\>x\<in\>\<bbb-X\>,s<around*|(|x|)>\<neq\>\<top\>>.
+
+  Les déductions de la forme <math|l\<Rightarrow\>s> signifient ``avec la
+  mémoire <math|l>, on peut déduire du système l'état (partiel) <math|s>''.
+  Les déductions de la forme <math|l,s\<vDash\>e\<rightarrow\><rsub|\<Sigma\>><rsup|v>v>
+  signifient ``avec la mémoire <math|l> et l'état partiellement calculé
+  <math|s>, l'expression <math|e> calculée dans le scope <math|\<Sigma\>>
+  prend la valeur <math|v>''.
+
+  <subsubsection|Règles de réduction pour l'activation du scope racine>
+
+  On note <math|i> les entrées du système à ce cycle ; on fait par définition
+  l'hypothèse <math|l\<Rightarrow\>i>, c'est-à-dire qu'on peut obtenir
+  l'environnement où seules les variables d'entrée sont définies. On
+  introduit ensuite la règle suivante, qui dit que le scope racine est
+  toujours actif et jamais reset par la suite :
+
+  <\equation*>
+    <frac|l\<Rightarrow\>s|l\<Rightarrow\>s<around*|[|act<rsub|/>\<assign\>t|]><around*|[|nreset<rsub|/>\<assign\>f|]>>
+  </equation*>
+
+  \;
+
+  <subsubsection|Règles de réduction pour l'init dans tous les scopes>
+
+  Pour tout scope <math|\<Sigma\>> défini dans le programme, qui est reset si
+  et seulement si la condition <math|l,s\<vDash\>r> est vraie, on rajoute les
+  règles de réduction suivantes qui permettent de déterminer si le scope est
+  init ou pas :
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\>r<rsub|\<Sigma\>>>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>t|]>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\><rsup|>\<neg\>r<rsub|\<Sigma\>>>|<cell|>|<cell|l<around*|(|act<rsub|\<Sigma\>>|)>=t>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>f|]>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\><rsup|>\<neg\>r<rsub|\<Sigma\>>>|<cell|>|<cell|l<around*|(|act<rsub|\<Sigma\>>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>l<around*|(|init<rsub|\<Sigma\>>|)>|]>>
+  </equation*>
+
+  \;
+
+  En particulier, pour le scope racine on instancie ces règles avec
+  <math|<around*|(|l,s\<vDash\>r<rsub|/>|)>\<Leftrightarrow\>l<around*|(|nreset<rsub|/>|)>=t>
+
+  <subsubsection|Règles de réduction d'expressions>
+
+  Ces règles permettent d'exprimer le calcul d'une expression. On note
+  <math|\<Sigma\>> le scope dans lequel l'expression est évaluée.
+
+  <\equation*>
+    <frac||l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>c>,c\<in\>\<bbb-V\>
+  </equation*>
+
+  <\equation*>
+    <frac|s<around*|(|x|)>\<neq\>\<top\>|l,s\<vDash\>x\<rightarrow\><rsup|v><rsub|\<Sigma\>>s<around*|(|x|)>>,x\<in\>\<bbb-X\>
+  </equation*>
+
+  <\equation*>
+    <frac||l,s\<vDash\>pre<rsub|i> e\<rightarrow\><rsup|v><rsub|\<Sigma\>>l<around*|(|m<rsub|i>|)>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l,s\<vDash\>e<rsub|1>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>>|<cell|>|<cell|l,s\<vDash\>e<rsub|2>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|2>>>>>>|l,s\<vDash\>e<rsub|1>\<odot\>e<rsub|2>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>\<odot\>v<rsub|2>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|s<around*|(|init<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>e<rsub|1>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>>>>>>|l,s\<vDash\><around*|(|e<rsub|1>\<rightarrow\>e<rsub|2>|)>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|s<around*|(|init<rsub|\<Sigma\>>|)>=f>|<cell|>|<cell|l,s\<vDash\>e<rsub|2>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|2>>>>>>|l,s\<vDash\><around*|(|e<rsub|1>\<rightarrow\>e<rsub|2>|)>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|2>>
+  </equation*>
+
+  <\equation*>
+    etc\<ldots\>
+  </equation*>
+
+  <subsubsection|Règles de réduction pour les pre>
+
+  Pour chaque expression <math|pre<rsub|i> e> introduite dans le scope
+  <math|\<Sigma\>>, on donne les deux règles suivante :
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>e\<rightarrow\><rsup|v><rsub|\<Sigma\>>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|i>\<assign\>v|]>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|i>\<assign\>l<around*|(|m<rsub|i>|)>|]>>
+  </equation*>
+
+  <subsubsection|Règles de réduction pour les affectations>
+
+  Pour toute affectation <math|x=e> apparaissant dans le scope
+  <math|\<Sigma\>>, on donne la règle suivante :
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>e\<rightarrow\><rsup|v><rsub|\<Sigma\>>v>>>>>|l\<Rightarrow\>s<around*|[|x\<assign\>v|]>>
+  </equation*>
+
+  <subsubsection|Règles de réduction pour les blocs activate>
+
+  Pour tout bloc <math|activate if c then b<rsub|1> else b<rsub|2>>
+  apparaissant dans le scope <math|\<Sigma\>>, on crée deux nouveaux scopes
+  <math|\<Sigma\><rsub|1>> et <math|\<Sigma\><rsub|2>> dans lesquels on
+  rajoute les règles de réductions pour <math|b<rsub|1>> et <math|b<rsub|2>>
+  respectivement, et on rajoute les règles suivantes qui régissent
+  l'activation des deux scopes <math|\<Sigma\><rsub|1>> et
+  <math|\<Sigma\><rsub|2>> :
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>f|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>f|]>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>t>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>t|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>f|]>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>f|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>t|]>>
+  </equation*>
+
+  Les deux scopes <math|\<Sigma\><rsub|1>> et <math|\<Sigma\><rsub|2>>
+  héritent de la condition de reset du scope <math|\<Sigma\>>.
+
+  <subsubsection|Règles de réduction pour les automates>
+
+  On note <math|A> l'automate, <math|s<rsub|0>> son état initial. Les règles
+  d'activation des différents scopes des états se font en fonction de la
+  variable <math|state<rsub|A>> définie pour l'automate <math|A> comme suit :
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\>r<rsub|\<Sigma\>>>>>>>|l\<Rightarrow\>s<around*|[|state<rsub|A>=s<rsub|0>|]>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\>\<neg\>r<rsub|\<Sigma\>>>>>>>|l\<Rightarrow\>s<around*|[|state<rsub|A>=l<around*|(|nstate<rsub|A>|)>|]>>
+  </equation*>
+
+  Puis pour chaque état <math|s<rsub|i>>, on définit <math|\<Sigma\><rsub|i>>
+  son scope dans lequel on traduit son corps, puis on rajoute la règle
+  d'activation suivante :
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|state<rsub|A>|)>=s<rsub|i>>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|i>>=t|]>>
+  </equation*>
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|state<rsub|A>|)>\<neq\>s<rsub|i>>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|i>>=f|]>>
+  </equation*>
+
+  Dans tous les scopes <math|\<Sigma\><rsub|i>>, la condition de reset peut
+  être éventuellement augmentée d'un <math|\<vee\>> avec une condition du
+  type <math|l<around*|(|nreset<rsub|\<Sigma\><rsub|i>>|)>=t>, où la variable
+  <math|nreset<rsub|\<Sigma\><rsub|i>>> est mise à true dès que l'on emprunte
+  une transition qui reset, et à false le reste du temps.
+
+  La règle pour une transition <math|s<rsub|i><long-arrow|\<rubber-rightarrow\>|c>s<rsub|j>>
+  sont du style :
+
+  <\equation*>
+    <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|state<rsub|A>|)>=s<rsub|i>>|<cell|>|<cell|l,s\<vDash\>c\<rightarrow\><rsub|\<Sigma\>><rsup|v>t>>>>>|l\<Rightarrow\>s<around*|[|nstate<rsub|A>\<assign\>s<rsub|j>|]>>
+  </equation*>
+
+  À cela, il faut rajouter les conditions qui disent que l'on emprune
+  exactement une transition à chaque cycle, ainsi que la partie qui définit
+  les variables <math|nreset<rsub|\<Sigma\><rsub|i>>>.
+
+  <\example>
+    On va écrire les règles de réduction qui définissent le programme suivant
+    :
+
+    <\verbatim-code>
+      node half() returns(c: int)
+
+      var half: bool;
+
+      \ \ \ \ a, b: int;
+
+      \ \ \ \ la, lb: int;
+
+      let
+
+      \ \ half = true -\<gtr\> not pre half;
+
+      \ \ activate
+
+      \ \ \ \ if half then let
+
+      \ \ \ \ \ \ \ \ a = la + 1;
+
+      \ \ \ \ \ \ \ \ b = lb;
+
+      \ \ \ \ tel else let
+
+      \ \ \ \ \ \ \ \ a = la;
+
+      \ \ \ \ \ \ \ \ b = lb + 1;
+
+      \ \ \ \ tel
+
+      \ \ returns a, b;
+
+      \ \ la = 0 -\<gtr\> pre a;
+
+      \ \ lb = 0 -\<gtr\> pre b;
+
+      \ \ c = a - b;
+
+      tel
+    </verbatim-code>
+
+    Les règles de calcul des expressions sont tout le temps les mêmes. Les
+    règles déduites de la structure du programme sont les suivantes :
+
+    Initialisation :
+
+    <\equation*>
+      <frac|l\<Rightarrow\>s|l\<Rightarrow\>s<around*|[|act<rsub|/>\<assign\>t|]><around*|[|nreset<rsub|/>\<assign\>f|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s
+      >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=t>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>t|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s
+      >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=f>|<cell|>|<cell|l<around*|(|act<rsub|/>|)>=t>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|/>\<assign\>f|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s
+      >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=f>|<cell|>|<cell|l<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|/>\<assign\>l<around*|(|init<rsub|/>|)>|]>>
+    </equation*>
+
+    Affectation <verbatim|c = a - b> :
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>a-b\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|c\<assign\>v|]>>
+    </equation*>
+
+    Affectations de <verbatim|la<math|>> et <verbatim|lb> :
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\><around*|(|0\<rightarrow\>pre<rsub|1>|)>
+      a\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|la\<assign\>v|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\><around*|(|0\<rightarrow\>pre<rsub|2>
+      b|)>\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|lb\<assign\>v|]>>
+    </equation*>
+
+    Affectation de <verbatim|half> :
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\><around*|(|true\<rightarrow\>not
+      pre<rsub|3> half|)>\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|half\<assign\>v|]>>
+    </equation*>
+
+    Mémorisation des valeurs pour <verbatim|pre a>, <verbatim|pre b> et
+    <verbatim|pre half> :
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>a\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|1>\<assign\>v|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>b\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|2>\<assign\>v|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|3>\<assign\>v|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|1>\<assign\>l<around*|(|m<rsub|1>|)>|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|2>\<assign\>l<around*|(|m<rsub|2>|)>|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|3>\<assign\>l<around*|(|m<rsub|3>|)>|]>>
+    </equation*>
+
+    Activation des deux moitiés du activate :
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\>t>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=t|]><around*|[|act<rsub|/2>\<assign\>f|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\>f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=f|]><around*|[|act<rsub|/2>\<assign\>t|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=f|]><around*|[|act<rsub|/2>\<assign\>f|]>>
+    </equation*>
+
+    Affectation de <verbatim|a> et <verbatim|b> dans la première moitié :
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/1>|)>=t>|<cell|>|<cell|l,s\<vDash\>la+1\<rightarrow\><rsub|/1><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|a\<assign\>v|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/1>|)>=t>|<cell|>|<cell|l,s\<vDash\>lb\<rightarrow\><rsub|/1><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|b\<assign\>v|]>>
+    </equation*>
+
+    Et dans la deuxième moitié :
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/2>|)>=t>|<cell|>|<cell|l,s\<vDash\>la\<rightarrow\><rsub|/2><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|a\<assign\>v|]>>
+    </equation*>
+
+    <\equation*>
+      <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/2>|)>=t>|<cell|>|<cell|l,s\<vDash\>lb+1\<rightarrow\><rsub|/2><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|b\<assign\>v|]>>
+    </equation*>
+
+    Et c'est tout.
+  </example>
+
+  (il faudrait faire un exemple avec des automates, mais ça risque d'être
+  encore plus long !)
+
+  <subsection|Sémantique par traduction, règles de traduction>
+
+  On définit la traduction de <math|P> en une formule
+  <math|F<around*|(|l,s|)>> comme suit.
+
+  <subsubsection|Traduction des expressions numériques et booléennes>
+
+  On utilise des formules ``à trous'' pour faire la traduction. Un trou
+  <math|\<box\>> correspond à la fonction <math|e\<mapsto\>e>, une formule
+  <math|a\<wedge\>x=\<box\>> correspond à la fonction
+  <math|e\<mapsto\>a\<wedge\>x=e>, etc. L'argument d'une fonction trou peut
+  aussi être un couple d'expressions, ainsi
+  <math|\<box\><rsub|1>+\<box\><rsub|2>> correspond à la fonction
+  <math|<around*|(|e,f|)>\<mapsto\>e+f>.
+
+  On définit la fonction <math|T<around*|(|\<Sigma\>,e,w|)>> comme étant la
+  traduction de l'expression <math|e> considérée dans le scope
+  <math|\<Sigma\>> et devant être placée dans le trou <math|w>. En pratique,
+  on divise <math|T> en deux fonctions, une pour les expressions booléennes
+  et une pour les expressions numériques. Le résultat d'une traduction doit
+  généralement être une formule booléenne.
+
+  On note <math|\<odot\>> n'importe quel opérateur binaire :
+  <math|+,-,\<times\>,/,mod,\<less\>,\<gtr\>,\<leqslant\>,\<geqslant\>,=,\<neq\>,\<wedge\>,\<vee\>>.
+
+  Les règles sont les suivantes :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|T<rsub|><around*|(|\<Sigma\>,<around*|(|e<rsub|1>,e<rsub|2>,\<ldots\>,e<rsub|n>|)>,w|)>>|<cell|=>|<cell|w<around*|[|T<rsub|><around*|(|\<Sigma\>,e<rsub|1>,\<box\>|)>,\<ldots\>,T<rsub|><around*|(|\<Sigma\>,e<rsub|n>,\<box\>|)>|]>>>|<row|<cell|\<forall\>c\<in\>\<bbb-V\>,<text|
+    \ \ \ \ \ \ \ >T<rsub|><around*|(|\<Sigma\>,c,w|)>>|<cell|=>|<cell|w<around*|[|c|]>>>|<row|<cell|\<forall\>x\<in\>\<bbb-X\>,<text|
+    \ \ \ \ \ \ >T<around*|(|\<Sigma\>,x,w|)>>|<cell|=>|<cell|w<around*|[|s<around*|(|x|)>|]>>>|<row|<cell|T<around*|(|\<Sigma\>,pre<rsub|i>
+    e,w|)>>|<cell|=>|<cell|w<around*|[|l<around*|(|m<rsub|i>|)>|]>>>|<row|<cell|T<around*|(|\<Sigma\>,e<rsub|1>\<rightarrow\>e<rsub|2>,w|)>>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,e<rsub|1>,w|)>|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,e<rsub|2>,w|)>|)>>>|<row|<cell|T<around*|(|\<Sigma\>,e<rsub|1>\<odot\>e<rsub|2>,w|)>>|<cell|=>|<cell|T<rsub|n><around*|(|\<Sigma\>,<around*|(|e<rsub|1>,e<rsub|2>|)>,w<around*|[|\<box\><rsub|1>\<odot\>\<box\><rsub|2>|]>|)>>>|<row|<cell|T<around*|(|\<Sigma\>,if
+    c then e<rsub|1> else e<rsub|2>,w|)>>|<cell|=>|<cell|<around*|(|T<around*|(|\<Sigma\>,c,\<box\>|)>\<wedge\>T<rsub|><around*|(|\<Sigma\>,e<rsub|1>,w|)>|)>\<vee\><around*|(|\<neg\>T<around*|(|\<Sigma\>,c,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,e<rsub|1>,w|)>|)>>>|<row|<cell|T<around*|(|\<Sigma\>,-e,w|)>>|<cell|=>|<cell|T<rsub|><around*|(|\<Sigma\>,e,w<around*|[|-\<box\>|]>|)>>>|<row|<cell|T<around*|(|\<Sigma\>,\<neg\>e,w|)>>|<cell|=>|<cell|T<rsub|><around*|(|\<Sigma\>,e,w<around*|[|\<neg\>\<box\>|]>|)>>>>>
+  </eqnarray*>
+
+  Par la suite, une affectation <math|x=e> sera traduite par la formule
+  booléenne <math|T<around*|(|\<Sigma\>,e,x=\<box\>|)>>.
+
+  <\example>
+    Effectuons par exemple la traduction de <math|x=if y\<geqslant\>0 then y
+    else -y> :
+
+    <\eqnarray*>
+      <tformat|<table|<row|<cell|F>|<cell|=>|<cell|T<around*|(|\<Sigma\>,if
+      y\<geqslant\>0 then y else -y,x=\<box\>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|T<around*|(|\<Sigma\>,y\<geqslant\>0,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,y,x=\<box\>|)>|)>\<vee\><around*|(|\<neg\>T<around*|(|\<Sigma\>,y\<geqslant\>0,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,-y,x=\<box\>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|y\<geqslant\>0\<wedge\>x=y|)>\<vee\><around*|(|\<neg\><around*|(|y\<geqslant\>0|)>\<wedge\>x=-y|)>>>>>
+    </eqnarray*>
+  </example>
+
+  <\example>
+    Effectuons la traduction de <math|x=0\<rightarrow\>pre<rsub|1> x + 1>.
+
+    <\eqnarray*>
+      <tformat|<table|<row|<cell|F>|<cell|=>|<cell|T<around*|(|\<Sigma\>,0\<rightarrow\>pre<rsub|1>x
+      + 1,s<around*|(|x|)>=\<box\>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,0,s<around*|(|x|)>=\<box\>|)>|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,pre<rsub|1>x
+      + 1,s<around*|(|x|)>=\<box\>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,<around*|(|pre<rsub|1>x,1|)>,s<around*|(|x|)>=\<box\><rsub|1>+\<box\><rsub|2>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\><around*|(|s<around*|(|x|)>=\<box\><rsub|1>+\<box\><rsub|2>|)><around*|(|T<around*|(|\<Sigma\>,pre<rsub|1>x,\<box\>|)>,T<around*|(|\<Sigma\>,1,\<box\>|)>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\><around*|(|s<around*|(|x|)>=\<box\><rsub|1>+\<box\><rsub|2>|)><around*|(|l<around*|(|m<rsub|1>|)>,1|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=l<around*|(|m<rsub|1>|)>+1|)>>>>>
+    </eqnarray*>
+
+    Remarque : dans une étape à part, il faut penser à mémoriser une valeur
+    pour <math|m<rsub|1>>, c'est-à-dire à introduire l'équation
+    <math|s<around*|(|m<rsub|1>|)>=s<around*|(|x|)>>
+  </example>
+
+  <subsubsection|Traduction de scopes et de programmes>
+
+  On définit une traduction complète pour les programmes, en pensant à
+  introduire les équations de persistance de la mémoire pour les pre. On
+  introduit aussi des équations qui déterminent si un scope est actif ou
+  inactif, si il est init ou pas, si il doit être reset ou pas, en fonction
+  des divers paramètres du programme (états d'automates, conditions de blocs
+  activate). De manière générale, un scope a deux traductions qui sont
+  produites : une pour le cas où ce scope est actif, et une pour le cas où il
+  est inactif (dans le cas inactif, il s'agit simplement de perpétuer les
+  mémoires). Ainsi la traduction d'un bloc ``<math|activate if c then
+  b<rsub|1> else b<rsub|2>>'' sera du style
+  <math|<around*|(|c\<wedge\>T<rsub|active><around*|(|b<rsub|1>|)>\<wedge\>T<rsub|inactive><around*|(|b<rsub|2>|)>|)>\<vee\><around*|(|\<neg\>c\<wedge\>T<rsub|active><around*|(|b<rsub|2>|)>\<wedge\>T<rsub|inactive><around*|(|b<rsub|1>|)>|)>>.
+
+  Tout cela est long à écrire, aussi nous nous contenterons de donner un
+  exemples.
+
+  <\example>
+    Traduction du programme :
+
+    <\verbatim-code>
+      node test() returns(x: int)
+
+      var lx: int;
+
+      let
+
+      \ \ lx = 0 -\<gtr\> pre x;
+
+      \ \ x = if lx \<gtr\>= 5 then 0 else lx + 1;
+
+      tel
+    </verbatim-code>
+
+    On obtient la formule :
+
+    <\eqnarray*>
+      <tformat|<table|<row|<cell|>|<cell|>|<cell|>>|<row|<cell|>|<cell|>|<cell|<around*|(|<stack|<tformat|<cwith|1|-1|2|2|cell-halign|l>|<table|<row|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>\<wedge\>s<around*|(|init<rsub|/>|)>>>|<row|<cell|\<vee\>>|<cell|\<neg\>l<around*|(|nreset<rsub|/>|)>\<wedge\><around*|(|<stack|<tformat|<cwith|1|-1|2|2|cell-halign|l>|<table|<row|<cell|>|<cell|l<around*|(|act<rsub|/>|)>\<wedge\>\<neg\>s<around*|(|init<rsub|/>|)>>>|<row|<cell|\<vee\>>|<cell|\<neg\>l<around*|(|act<rsub|/>|)>\<wedge\>s<around*|(|init<rsub|/>|)>=l<around*|(|init<rsub|/>|)>>>>>>|)>>>>>>|)>>>|<row|<cell|>|<cell|\<wedge\>>|<cell|s<around*|(|act<rsub|/>|)>>>|<row|<cell|>|<cell|\<wedge\>>|<cell|\<neg\>s<around*|(|nreset<rsub|/>|)>>>|<row|<cell|>|<cell|\<wedge\>>|<cell|<around*|(|s<around*|(|init<rsub|/>|)>\<wedge\>s<around*|(|lx|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|/>|)>\<wedge\>s<around*|(|lx|)>=l<around*|(|m<rsub|1>|)>|)>>>|<row|<cell|>|<cell|\<wedge\>>|<cell|<around*|(|s<around*|(|lx|)>\<geqslant\>5\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|s<around*|(|lx|)>\<less\>5\<wedge\>s<around*|(|x|)>=s<around*|(|lx|)>+1|)>>>|<row|<cell|>|<cell|\<wedge\>>|<cell|s<around*|(|m<rsub|1>|)>=s<around*|(|x|)>>>>>
+    </eqnarray*>
+  </example>
+
+  Pour d'autres traductions, voir les sorties produites par
+  <verbatim|scade-analyzer>.
+
+  <section|Interprète pour sémantique concrète>
+
+  Une première façon de faire un interprète pour la sémantique concrète
+  serait de faire un interprète de formules logiques, et d'appliquer la
+  formule obtenue par traduction répétitivement jusqu'à obtenir un point
+  fixe.
+
+  Ce n'est cependant pas cette solution que nous avons choisi de mettre en
+  place, notre solution est plus proche de la sémantique par réduction
+  définie plus haut.
+
+  Nous avons choisi de représenter un état <math|s> du programme en cours de
+  calcul comme une valeur mutables, où les variables sont calculées au fur et
+  à mesure qu'on les demande. La structure <math|s> peut donc contenir à un
+  instant donné pour une certaine variable soit une valeur, soit une fonction
+  à appeller pour que cette valeur soit calculée et rajoutée à <math|s>.
+
+  La procédure de calcul consiste à activer le scope racine, puis à appeller
+  les fonctions de calcul sur les variables de sortie jusqu'à ce qu'on
+  obtienne des valeurs. On enregistre ensuite la portion d'état qui nous
+  intéresse pour le cycle suivant.
+
+  L'activation d'un scope se fait selon la procédure suivante :
+
+  <\itemize>
+    <item>Pour une affectation <math|x=e>, rajouter dans <math|s> pour la
+    variable <math|x> la fonction qui calcule <math|e> et rajoute la valeur
+    trouvée dans <math|s>.
+
+    <item>Pour un bloc activate, rajouter dans <math|s> pour toutes les
+    variables returnées par le bloc, la fonction qui choisit la branche à
+    activer en calculant les conditions et active le scope correspondant.
+
+    <item>Pour un automate, rajouter dans <math|s> pour toutes les variables
+    returnées par l'automate, la fonction qui choisit l'état à activer en se
+    basant sur l'état enregistré au cycle précédent, et active le scope
+    correspondant.
+  </itemize>
+
+  L'étape d'enregistrement des variables d'intérêt pour le cycle suivant
+  comporte notamment une phase de calcul des transitions faibles empruntées
+  par les automates du programme, pour qu'à l'étape suivante le calcul puisse
+  reprendre directement. Les restart sont aussi traités à ce moment là, avec
+  une fonction pour reset un scope qui remet toutes les variables init à true
+  et tous les états à l'état initial, récursivement.
+
+  <section|Interprétation abstraite>
+
+  \;
+
+  <underline|<verbatim|/!\\>> <strong|travaux travaux travaux>
+  <verbatim|<underline|/!\\>>
+
+  \;
+
+  \;
+
+  Le but de l'interprétation abstraite est de prouver certaines propriétés
+  sur un programme. Pour cela, nous passons par une première approximation,
+  la sémantique collectrice, que nous approximons une seconde fois en la
+  passant dans un domaine de représentation abstraite.
+
+  <subsection|Sémantique collectrice>
+
+  <subsubsection|Nouvelle notation : fonction de transition>
+
+  Notons <math|\<bbb-X\>> l'ensemble des variables. On note
+  <math|\<bbb-X\>=\<bbb-X\><rsub|e>\<cup\>\<bbb-X\><rsub|n>> : c'est l'union
+  des variables de type énumération et des variables de \ type numérique.
+
+  Un état du système est une fonction <math|\<bbb-X\>\<rightarrow\>\<bbb-V\>>,
+  où <math|\<bbb-V\>> représente l'ensemble des valeurs (numériques ou
+  énumération). On note <math|\<bbb-M\>=\<bbb-X\>\<rightarrow\>\<bbb-V\>>
+  l'ensemble des états du système.
+
+  Avant le premier cycle, le système peut être dans n'importe quel état de
+  <math|I> :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|I>|<cell|=>|<cell|<around*|{|s\<in\>\<bbb-M\>
+    \| s<around*|(|nreset<rsub|/>|)>=t|}>>>>>
+  </eqnarray*>
+
+  Entre deux cycles, les variables qui comptent réellement dans <math|s> sont
+  les variables actif et reset pour les scopes, les variables d'état pour les
+  automates, et les valeurs des <em|pre>.
+
+  Vision habituelle : on a une suite d'états
+  <math|s<rsub|0>,s<rsub|1>,\<ldots\>> qui représentent la mémoire entre deux
+  cycles. <math|s<rsub|0>> est défini. On a une relation de transition qui
+  prend <math|s<rsub|n>> et les entrées <math|i<rsub|n+1>> et qui calcule les
+  sorties <math|o<rsub|n+1>> et l'état suivant <math|s<rsub|n+1>> :
+
+  <\equation*>
+    s<rsub|0><long-arrow|\<rubber-rightarrow\>|i<rsub|1>>o<rsub|1>,s<rsub|1><long-arrow|\<rubber-rightarrow\>|i<rsub|2>>o<rsub|2>,s<rsub|2><long-arrow|\<rubber-rightarrow\>|i<rsub|3>>o<rsub|3>,s<rsub|3>\<rightarrow\>*\<cdots\>*
+  </equation*>
+
+  Nous introduisons ici une seconde notation pour ce fonctionnement.
+
+  Les variables de l'état précédent <math|s<rsub|n-1>>, au lieu d'être
+  considérées comme un lieu à part, sont partiellement copiées dans l'état
+  <math|s<rsub|n>> par une fonction que l'on appellera fonction de cycle.
+  Cette fonction copie uniquement les variables dont les valeurs précédentes
+  sont utiles pour le calcul de la transition, et préfixe leur noms d'un
+  prefixe standard, ``L'', qui indique que ce sont des variables <em|last>,
+  c'est-à-dire qu'on a leur valeur du cycle précédent.
+
+  La fonction de cycle <math|c : \<bbb-M\>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>>
+  s'occupe de faire passer les valeurs suivantes aux valeurs actuelles (nous
+  écrivons cette fonction comme non-déterministe car après cette fonction un
+  certain nombre de variables sont oubliées et on considère que leurs valeurs
+  n'ont pas d'importance). Elle peut être définie à partir d'un ensembles de
+  variables <math|C>, qui sont les variables qui nous intéresseront lors du
+  calcul de la transition :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|c<around*|(|s|)>>|<cell|=>|<cell|<around*|{|s<rprime|'>\<in\>\<bbb-M\>
+    \| \<forall\>x\<in\>C,s<rprime|'><around*|(|L
+    x|)>=s<around*|(|x|)>|}>>>>>
+  </eqnarray*>
+
+  \;
+
+  Déroulement d'un cycle : on prend l'état <math|s> après passage par la
+  fonction de cycle, on y met les valeurs des entrées du système. On applique
+  ensuite la fonction <math|f : \<bbb-M\>\<rightarrow\>\<bbb-M\>> qui calcule
+  toutes les variables du système (elle peut être définie comme la saturation
+  de la sémantique par réduction, comme le point fixe de l'application d'une
+  formule, ou plus classiquement comme l'application d'une série
+  d'instructions en style impératif, résultat de la compilation du
+  programme). On peut à ce moment récupérer les valeurs de sorties.
+
+  Avec nos notations : <math|o<rsub|n+1>> est la restriction de
+  <math|f<around*|(|c<around*|(|s<rsub|n>|)>+i<rsub|n+1>|)>> aux variables de
+  sortie , où <math|c<around*|(|s<rsub|n>|)>+i<rsub|n+1>> correspond à
+  définir les variables de <math|c<around*|(|s<rsub|n>|)>> et de
+  <math|i<rsub|n+1>>.
+
+  <\remark>
+    En principe, quel que soit <math|x\<in\>c<around*|(|s<rsub|n>|)>>,
+    <math|f<around*|(|x+i<rsub|n+1>|)>> ne peut être qu'un seul
+    environnement, car le programme est déterministe. C'est pourquoi on se
+    permet l'abus de notation <math|f<around*|(|c<around*|(|s<rsub|n>|)>+i<rsub|n+1>|)>>.
+  </remark>
+
+  <subsubsection|Suppression des entrées, sémantique collectrice>
+
+  On s'intéresse maintenant à l'exécution d'un programme SCADE quel que
+  soient ses entrées <math|i<rsub|n>>. On peut faire des hypothèses sur ces
+  entrées en utilisant la directive <verbatim|assume> du langage. On suppose
+  que l'on dispose d'une fonction <math|q :
+  \<bbb-M\>\<rightarrow\><around*|{|t,f|}>> qui nous dit si un environnement
+  est conforme à la spécification.
+
+  On s'intéresse maintenant à la sémantique non déterministe suivante :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|<around*|{|s\<in\>\<bbb-M\>
+    \| s<around*|(|nreset<rsub|/>|)>=t|}>>>|<row|<cell|s<rsub|n+1><rsub|>>|<cell|=>|<cell|g<around*|(|s<rsub|n>|)>>>|<row|<cell|g<around*|(|x|)>>|<cell|=>|<cell|<big|cup><rsub|s\<in\>x><around*|{|f<around*|(|a|)>,a\<in\>c<around*|(|s|)>,q<around*|(|f<around*|(|a|)>|)>=t|}>>>>>
+  </eqnarray*>
+
+  \;
+
+  La valeur <math|s<rsub|n>> contient tous les environnements possibles pour
+  le système à la <math|n>-ème étape, quelles que soient les entrées jusque
+  là.
+
+  On définit maintenant la sémantique collectrice du programme comme étant la
+  valeur :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|S>|<cell|=>|<cell|lfp<rsub|s<rsub|0>>
+    <around*|(|\<lambda\>s.s<rsub|0>\<cup\>g<around*|(|s|)>|)>>>|<row|<cell|S>|<cell|\<in\>>|<cell|\<cal-P\><around*|(|\<bbb-M\>|)>>>>>
+  </eqnarray*>
+
+  <math|S> représente ici exactement l'ensemble de tous les états accessibles
+  par le système, à tout moment, quelles que soient les valeurs en entrée.
+
+  Toute la suite de notre travail consistera à construire une approximation
+  la meilleure possible de <math|S>.
+
+  <subsection|Généralités sur l'interprétation abstraite>
+
+  Une abstraction est définie par une correspondance de Galois entre
+  <math|\<cal-P\><around*|(|\<bbb-M\>|)>> et <math|\<cal-D\><rsup|#>>,
+  représentation abstraite d'une partie de <math|\<bbb-M\>>. L'abstraction
+  peut être caractérisée par sa fonction de concrétisation :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<gamma\><rsub|\<bbb-M\>>>|<cell|:>|<cell|\<cal-D\><rsup|#>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>>>>>
+  </eqnarray*>
+
+  \ On peut aussi généralement s'appuyer sur l<math|>'existence d'une
+  fonction d'abstraction :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<alpha\><rsub|\<bbb-M\>>>|<cell|:>|<cell|\<cal-P\><around*|(|\<bbb-M\>|)>\<rightarrow\>\<cal-D\><rsup|#>>>>>
+  </eqnarray*>
+
+  Cette fonction fait correspondre à une partie de <math|\<bbb-M\>> sa
+  meilleure approximation dans le domaine abstrait (par exemple dans le cas
+  des polyhèdres, l'abstraction d'un ensemble fini de points est leur
+  enveloppe convexe, mais un cercle n'a pas de meilleure abstraction).
+
+  Dans tous les cas, on s'attend à ce que
+  <math|\<forall\>x\<in\>\<cal-D\><rsup|#>,x\<sqsubseteq\>\<alpha\><around*|(|\<gamma\><around*|(|x|)>|)>>
+  d'une part et <math|\<forall\>y\<in\>\<cal-P\><around*|(|\<bbb-M\>|)>,y\<subseteq\>\<gamma\><around*|(|\<alpha\><around*|(|y|)>|)>>
+  d'autre part.
+
+  De base ici, nous avons deux choix simples pour <math|\<cal-D\><rsup|#>> :
+  les intervalles et les polyhèdres convexes. Ceux-ci sont considérés acquis
+  pour la suite ; on les note <math|\<cal-D\><rsub|int><rsup|#>> et
+  <math|\<cal-D\><rsub|poly><rsup|#>>, avec les fonctions de concrétisation
+  <math|\<gamma\><rsub|int>> et <math|\<gamma\><rsub|poly>> associées.
+
+  On note <math|\<bbb-E\>> l'ensemble des égalités et inégalités sur des
+  variables de <math|\<bbb-X\>>. Par exemple les éléments suivants sont des
+  équations de <math|\<bbb-E\>> : <math|x=0,c=tt,y\<geqslant\>5*x-2>.
+
+  Pour <math|s\<in\>\<bbb-M\>> et <math|e\<in\>\<bbb-E\>>, on note
+  <math|s\<vDash\>e> si l'expression <math|e> est vraie dans l'état <math|s>.
+
+  Pour un domaine abstrait <math|\<cal-D\><rsup|#>> et pour une expression
+  <math|e\<in\>\<bbb-E\>>, on suppose que l'on a une fonction sémantique
+  <math|<around*|\<llbracket\>|e|\<rrbracket\>> :
+  \<cal-D\><rsup|#>\<rightarrow\>\<cal-D\><rsup|#>> qui restreint
+  l'abstraction <math|s<rsup|#>> en une sur-approximation (la meilleure
+  possible) de <math|\<alpha\><around*|(|<around*|{|s\<in\>\<gamma\><around*|(|s<rsup|#>|)>
+  \| s\<vDash\>e|}>|)>> :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|<around*|{|s\<in\>\<gamma\><around*|(|s<rsup|#>|)>
+    \| s\<vDash\>e|}>>|<cell|\<sqsubseteq\>>|<cell|\<gamma\><around*|(|<around*|\<llbracket\>|e|\<rrbracket\>><around*|(|s<rsup|#>|)>|)>>>>>
+  </eqnarray*>
+
+  La fonction de transition <math|f> est représentée dans l'abstrait par une
+  fonction <math|f<rsup|#>> qui correspond à l'application d'un certain
+  nombre de contraintes de <math|\<bbb-E\>>, ainsi que de disjonction de cas.
+  On remarque que l'aspect impératif disparait complètement, on n'a plus
+  qu'un ensemble d'équations et de disjonctions. La traduction du programme
+  SCADE en formule logique donne directement une formule de ce style que l'on
+  peut appliquer sur un environnement abstrait.
+
+  La fonction de cycle <math|c> correspond à conserver un certain nombre de
+  variables en tant que \S mémoires \T, en préfixant leur noms d'un \S L \T
+  pour <em|last>. Notons <math|C> l'ensemble des variables à conserver. Cette
+  fonction peut être représentée dans l'abstrait par l'opérateur
+  <math|c<rsup|#>> dont une définition est :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|c<rsup|#><around*|(|s|)>>|<cell|=>|<cell|\<alpha\><around*|(|<around*|{|\<rho\>\<in\>\<bbb-M\>
+    \| \<forall\>x\<in\>C,\<exists\>\<rho\><rprime|'>\<in\>\<gamma\><around*|(|s|)>\|\<rho\><around*|(|L
+    x|)>=\<rho\><rprime|'><around*|(|x|)>|}>|)>>>>>
+  </eqnarray*>
+
+  (cette définition n'est pas constructive car on n'implémente jamais
+  <math|\<gamma\>> directement)
+
+  Cela correspond à oublier un certain nombre de variables qui ne nous
+  intéressent plus, et à renommer celles que l'on garde.
+
+  Par facilité, on note <math|g<rsup|#>=c<rsup|#>\<circ\>f<rsup|#>>. Étant
+  donné qu'un programme est essentiellement une grosse boucle, la valeur qui
+  nous intéresse est l'abstraction de <math|S> donnée par :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|S<rsup|#>>|<cell|=>|<cell|lfp<rsub|I<rsup|#>><around*|(|\<lambda\>i.I<rsup|#>\<sqcup\>g<rsup|#><around*|(|i|)>|)>>>>>
+  </eqnarray*>
+
+  Où <math|s<rsub|0>> est l'état initial du système et est défini par
+  <math|I<rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><around*|(|\<top\>|)>>,
+  où <math|i> est une équation du type <math|Lnreset<rsub|/>=tt>.
+
+  Nous en venons donc à chercher des domaines abstraits les mieux à même de
+  représenter les différentes contraintes exprimables dans <math|\<bbb-E\>>.
+  Dans notre cas, celles-ci se divisent essentiellement en deux catégories :
+
+  <\itemize>
+    <item>Contraintes numériques : les variables sont dans
+    <math|\<bbb-X\><rsub|n>>, les constantes dans <math|\<bbb-N\>> (ou
+    <math|\<bbb-Q\>>), les opérateurs sont
+    <math|+,-,\<times\>,\<div\>,=,\<geqslant\>,\<neq\>>. On note
+    <math|\<bbb-E\><rsub|n>> l'ensemble de telles contraintes.
+
+    <item>Contraintes énumérées : les variables sont dans
+    <math|\<bbb-X\><rsub|e>>, les constantes dans un ensemble fini qui dépend
+    du types des variables, les opérateurs sont <math|\<equiv\>,\<nequiv\>>.
+    On note <math|\<bbb-E\><rsub|e>> l'ensemble de telles contraintes.
+  </itemize>
+
+  Les domaines numériques <math|\<cal-D\><rsub|int><rsup|#>> et
+  <math|\<cal-D\><rsub|poly><rsup|#>> ne sont pas à même de représenter
+  correctement les contraintes de <math|\<bbb-E\><rsub|e>>. Généralement, on
+  définit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<forall\>e\<in\>\<bbb-E\><rsub|e>\<nocomma\>,<around*|\<llbracket\>|e|\<rrbracket\>><rsub|int>>|<cell|=>|<cell|id<rsub|\<cal-D\><rsub|int><rsup|#>>>>|<row|<cell|\<forall\>e\<in\>\<bbb-E\><rsub|e>,<around*|\<llbracket\>|e|\<rrbracket\>><rsub|poly>>|<cell|=>|<cell|id<rsub|\<cal-D\><rsub|poly><rsup|#>>>>>>
+  </eqnarray*>
+
+  Les variables booléennes peuvent être représentées par <math|0> et
+  <math|1>, par exemple on peut introduire les restrictions suivantes (en
+  notant <math|\<bbb-X\><rsub|b>> l'ensemble des variables à valeurs
+  booléennes) :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<forall\>x\<in\>\<bbb-X\><rsub|b>,<around*|\<llbracket\>|x=tt|\<rrbracket\>>>|<cell|=>|<cell|<around*|\<llbracket\>|x=1|\<rrbracket\>><rsub|poly>>>|<row|<cell|\<forall\>x\<in\>\<bbb-X\><rsub|b>,<around*|\<llbracket\>|x=ff|\<rrbracket\>>>|<cell|=>|<cell|<around*|\<llbracket\>|x=0|\<rrbracket\>><rsub|poly>>>|<row|<cell|\<forall\>x,y\<in\>\<bbb-X\><rsub|b>,<around*|\<llbracket\>|x=y|\<rrbracket\>>>|<cell|=>|<cell|<around*|\<llbracket\>|x=y|\<rrbracket\>><rsub|poly>>>|<row|<cell|\<forall\>x,y\<in\>\<bbb-X\><rsub|b>,<around*|\<llbracket\>|x\<neq\>y|\<rrbracket\>>>|<cell|=>|<cell|<around*|\<llbracket\>|x=1-y|\<rrbracket\>><rsub|poly>>>>>
+  </eqnarray*>
+
+  Les résultats sont généralement plus que médiocres. De plus, on ne peut pas
+  représenter ainsi les valeurs d'énumérations ayant plus de deux éléments.
+
+  <section|Domaines abstraits et disjonction de cas>
+
+  Pour l'analyse de programmes SCADE, l'analyse de l'ensemble de la boucle de
+  contrôle comme une seule valeur dans un environnement abstrait numérique
+  est insuffisante. Il nous a donc été crucial de développer deux domaines
+  abstraits capables de faire des disjonctions de cas afin de traiter de
+  manière plus fine l'évolution du programme.
+
+  Nous souhaitons pouvoir faire des disjonctions de cas selons les valeurs
+  des variables de <math|\<bbb-X\><rsub|e>>. Par exemple si on a un automate
+  <math|A> dont la variable d'état s'appelle <math|q> et évolue dans
+  l'ensemble <math|Q=<around*|{|up,down,left,right,stay|}>>, on voudrait
+  pouvoir isoler cette variable des autres, ne plus l'inclure dans le domaine
+  abstrait et l'utiliser pour différencier plusieurs valeurs abstraites. Il
+  nous faut donc redéfinir le domaine abstrait <math|\<cal-D\>> et surtout la
+  fonction d'application d'une condition <math|<around*|\<llbracket\>|e|\<rrbracket\>>>.
+
+  <subsection|Domaine à disjonction simple>
+
+  Supposons que l'on ait maintenant trois ensembles de variables :
+
+  <\itemize>
+    <item><math|\<bbb-X\><rsub|n>> : variables numériques
+
+    <item><math|\<bbb-X\><rsub|e>> : variables énumérées non considérées
+    comme variables de disjonction
+
+    <item><math|\<bbb-X\><rsub|d>> : variables de disjonction, prenant leurs
+    valeurs dans <math|\<bbb-V\><rsub|d>> un ensemble fini (pour être précis,
+    il faudrait noter <math|\<forall\>x\<in\>\<bbb-X\><rsub|d>>,
+    <math|\<bbb-V\><rsub|d><around*|(|x|)>> l'ensemble des valeurs possibles
+    pour la valeur <math|x>, qui peut être différent selon la variable - on
+    est ammené à faire un peu de typage, il faut en particulier s'assurer que
+    les contraintes que l'on donne sont entre deux variables pouvant prendre
+    les mêmes valeurs).
+  </itemize>
+
+  On considère dans cette section que l'on a un domaine abstrait
+  <math|\<cal-D\><rsup|#>> capable de gérer les contraintes sur les variables
+  numériques et sur les variables énumérées, mais sans relation entre les
+  deux. Le domaine <math|\<cal-D\><rsup|#>> représente une abstraction de
+  <math|\<bbb-M\><rsub|n>=<around*|(|\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>|)>\<rightarrow\>\<bbb-V\>>.
+  On note <math|\<bot\><rsub|n>> et <math|\<top\><rsub|n>> les éléments
+  bottom et top de ce treillis, <math|\<sqcup\><rsub|d>> et
+  <math|\<sqcap\><rsub|d>> les bornes inf et sup de ce treillis.
+
+  La particularité des variables d'état est que l'on ne réalise pas
+  d'abstraction sur celles-ci : on représente directement un état par une
+  valuation de ces variables, dans <math|\<bbb-X\><rsub|d>\<rightarrow\>\<bbb-V\><rsub|d>=\<bbb-M\><rsub|d>>.
+  On peut le munir d'une structure de treillis :
+  <math|\<bbb-M\><rsub|d>\<cup\><around*|{|\<bot\>,\<top\>|}>> forme un
+  treillis plat : <math|\<forall\>x,y\<in\>\<bbb-M\><rsub|d>,x\<sqsubseteq\>y\<Leftrightarrow\>x=y>,
+  <math|\<forall\>x\<in\>\<bbb-M\><rsub|d>,\<bot\>\<sqsubset\>x\<sqsubset\>\<top\>>
+  (l'utilité de cette structure n'apparait pas.)
+
+  On appelle toujours <math|\<bbb-M\>=\<bbb-X\>\<rightarrow\>\<bbb-V\>>, où
+  <math|\<bbb-X\>=\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>\<cup\>\<bbb-X\><rsub|d>>.
+  On a une injection évidente de <math|\<bbb-M\><rsub|d>> dans
+  <math|\<cal-P\><around*|(|\<bbb-M\>|)>>, on identifie donc
+  <math|d\<in\>\<bbb-M\><rsub|d>> à <math|<around*|{|s\<in\>\<bbb-M\>\|\<forall\>x\<in\>\<bbb-X\><rsub|d>,s<around*|(|x|)>=\<bbb-M\><rsub|d><around*|(|x|)>|}>>.
+  De même on identifie <math|e\<in\>\<bbb-M\><rsub|n>> à
+  <math|<around*|{|s\<in\>\<bbb-M\> \| \<forall\>x\<in\>\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>,s<around*|(|x|)>=\<bbb-M\><rsub|n><around*|(|x|)>|}>>.
+
+  On construit maintenant le domaine abstrait disjonctif comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<cal-D\><rsub|d><rsup|#>>|<cell|=>|<cell|\<bbb-M\><rsub|d>\<rightarrow\>\<cal-D\><rsup|#>>>|<row|<cell|\<gamma\><rsub|d><around*|(|s|)>>|<cell|=>|<cell|<big|cup><rsub|d\<in\>\<bbb-M\><rsub|d>>d\<cap\>\<gamma\><around*|(|s<around*|(|d|)>|)>>>>>
+  </eqnarray*>
+
+  Les éléments <math|\<top\>> et <math|\<bot\>> sont définis comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<bot\><rsub|d>>|<cell|=>|<cell|\<lambda\>d.\<bot\><rsub|n>>>|<row|<cell|\<top\><rsub|d>>|<cell|=>|<cell|\<lambda\>d.\<top\><rsub|n>>>>>
+  </eqnarray*>
+
+  On vérifie bien que <math|\<gamma\><rsub|d><around*|(|\<bot\><rsub|d>|)>=\<varnothing\>>
+  et <math|\<gamma\><rsub|d><around*|(|\<top\><rsub|d>|)>=\<bbb-M\>>.
+
+  On peut aussi définir les opérations <math|\<sqcup\>> et <math|\<sqcap\>> :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s\<sqcup\>t>|<cell|=>|<cell|\<lambda\>d.<around*|(|s<around*|(|d|)>\<sqcup\><rsub|n>t<around*|(|d|)>|)>>>|<row|<cell|s\<sqcap\>t>|<cell|=>|<cell|\<lambda\>d.<around*|(|s<around*|(|d|)>\<sqcap\><rsub|n>t<around*|(|d|)>|)>>>>>
+  </eqnarray*>
+
+  Enfin, la partie intéressante : on peut définir un certain nombres
+  d'opérateurs de restriction :
+
+  <\itemize>
+    <item><math|\<forall\>x,y\<in\>\<bbb-X\><rsub|d>,\<forall\>s\<in\>\<cal-D\><rsub|d><rsup|#>>,
+
+    <\eqnarray*>
+      <tformat|<table|<row|<cell|<around*|\<llbracket\>|x=y|\<rrbracket\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si
+      d<around*|(|x|)>=d<around*|(|y|)>>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>|<row|<cell|<around*|\<llbracket\>|x\<neq\>y|\<rrbracket\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si
+      d<around*|(|x|)>\<neq\>d<around*|(|y|)>>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>>>
+    </eqnarray*>
+
+    <item><math|\<forall\>x\<in\>\<bbb-X\><rsub|d>,\<forall\>v\<in\>\<bbb-V\><rsub|d>>,
+
+    <\eqnarray*>
+      <tformat|<table|<row|<cell|<around*|\<llbracket\>|x=v|\<rrbracket\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si
+      d<around*|(|x|)>=v>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>|<row|<cell|<around*|\<llbracket\>|x\<neq\>v|\<rrbracket\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si
+      d<around*|(|x|)>\<neq\>v>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>>>
+    </eqnarray*>
+  </itemize>
+
+  <math|<around*|\<llbracket\>|e|\<rrbracket\>>> est donc défini correctement
+  pour tout <math|e\<in\>\<bbb-E\><rsub|d>>, où <math|\<bbb-E\><rsub|d>> est
+  l'ensemble des conditions sur variables de disjonction. Pour toute
+  expression <math|e\<in\>\<bbb-E\><rsub|n>> ou
+  <math|e\<in\>\<bbb-E\><rsub|e>>, le domaine <math|\<cal-D\><rsup|#>> est
+  sensé savoir les prendre en compte de manière satisfaisante, on définit
+  donc :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<forall\>e\<in\>\<bbb-E\><rsub|n>\<cup\>\<bbb-E\><rsub|e>,<around*|\<llbracket\>|e|\<rrbracket\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<around*|\<llbracket\>|e|\<rrbracket\>><around*|(|s<around*|(|d|)>|)>>>>>
+  </eqnarray*>
+
+  L'opérateur de widening reste problématique. On peut définir un opérateur
+  de widening point par point :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s \<nabla\><rsub|d>
+    t>|<cell|=>|<cell|\<lambda\>d.s<around*|(|d|)>\<nabla\>t<around*|(|d|)>>>>>
+  </eqnarray*>
+
+  Mais celui-ci est peu satisfaisant car chaque état
+  <math|d\<in\>\<bbb-M\><rsub|d>> représente potentiellement un état d'un
+  système de transitions, pouvant déboucher sur lui-même ou sur un autre
+  état, et il faut savoir prendre en compte ces disjonctions à un niveau plus
+  fin. Il faut donc plutôt voir le tout comme un système de transitions.
+
+  Étant donné notre système représenté par une fonction de transition
+  <math|f<rsup|#>> et une fonction de cycle <math|c<rsup|#>> (par facilité,
+  on notera <math|g<rsup|#>=c<rsup|#>\<circ\>f<rsup|#>>), l'ensemble des
+  états accessible par le système est <math|S<rsup|#>=lfp<rsub|I<rsup|#>><around*|(|\<lambda\>s.I<rsup|#>\<sqcup\>g<rsup|#><around*|(|s|)>|)>>,
+  où <math|I<rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><rsub|d><around*|(|\<top\><rsub|d>|)>>.
+
+  Définitions : pour <math|d<rsub|0>\<in\>\<bbb-M\><rsub|d>>, notons
+  <math|r<rsub|d<rsub|0>> : \<cal-D\><rsub|d><rsup|#>\<rightarrow\>\<cal-D\><rsub|d><rsup|#>>
+  tel que <math|r<rsub|d<rsub|0>><around*|(|s|)>=\<lambda\>d.<choice|<tformat|<table|<row|<cell|\<bot\>>|<cell|si
+  d\<neq\>d<rsub|0>>>|<row|<cell|s<around*|(|d|)>>|<cell|si d=d<rsub|0>>>>>>>
+
+  Le principe des itérations chaotiques peut s'écrire comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+    s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|n>|}>>>>>
+  </eqnarray*>
+
+  Tant que <math|\<delta\><rsub|n>\<neq\>\<varnothing\>>, on répète le
+  processus suivant :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|a<rsub|n+1>>|<cell|\<in\>>|<cell|\<delta\><rsub|n>
+    <text| (choisi arbitrairement)>>>|<row|<cell|D<rsub|n+1>>|<cell|=>|<cell|g<rsup|#><around*|(|r<rsub|a<rsub|n+1>><around*|(|s<rsub|n>|)>|)>>>|<row|<cell|s<rsub|n+1>>|<cell|=>|<cell|s<rsub|n>\<sqcup\>D<rsub|n+1>>>|<row|<cell|\<delta\><rsub|n+1>>|<cell|=>|<cell|<around*|(|\<delta\><rsub|n>\\<around*|{|a<rsub|n+1>|}>|)>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\|s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n><around*|(|d|)>|}>>>>>
+  </eqnarray*>
+
+  Intuitivement : <math|\<bbb-M\><rsub|d>> représente l'ensemble des états
+  possibles pour notre système de transition. À chaque itération, on choisit
+  un état qui a grossi depuis la dernière fois. On calcule ses successeurs et
+  on met à jour l'ensemble des états que l'on connait.
+
+  Problème : ici on ne fait pas de widening, et on peut être à peu près sûr
+  que l'analyse ne terminera pas (sauf cas simples). Pour cela, on introduit
+  un ensemble <math|K<rsub|\<nabla\>>\<subset\>\<bbb-M\><rsub|d>> qui
+  représente l'ensemble des états que l'on devra faire grossir par widening
+  et non par union simple dans le futur. La définition devient alors :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+    s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|n>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>>
+  </eqnarray*>
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|a<rsub|n+1>>|<cell|\<in\>>|<cell|\<delta\><rsub|n>
+    <text| (choisi arbitrairement)>>>|<row|<cell|D<rsub|n+1>>|<cell|=>|<cell|g<rsup|#><around*|(|r<rsub|a<rsub|n+1>><around*|(|s<rsub|n>|)>|)>>>|<row|<cell|s<rsub|n+1>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<rsub|n><around*|(|d|)>\<nabla\>D<rsub|n+1><around*|(|d|)>>|<cell|si
+    d\<in\>K<rsub|\<nabla\>,n>>>|<row|<cell|s<rsub|n><around*|(|d|)>\<sqcup\>D<rsub|n+1><around*|(|d|)>>|<cell|sinon>>>>>>>|<row|<cell|K<rsub|\<nabla\>,n+1>>|<cell|=>|<cell|K<rsub|\<nabla\>,n>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+    s<rsub|n><around*|(|d|)>\<neq\>\<bot\>\<wedge\>s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n>|}>>>|<row|<cell|\<delta\><rsub|n+1>>|<cell|=>|<cell|<around*|(|\<delta\><rsub|n>\\<around*|{|a<rsub|n+1>|}>|)>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\|s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n><around*|(|d|)>|}>>>>>
+  </eqnarray*>
+
+  Ie : si un état est apparu à une étape, et si à une étape ultérieure il
+  grossit, alors lors de toutes les étapes suivantes on le fera grossir non
+  pas par union simple mais par élargissement.
+
+  Reste une question : comment prendre en compte les conditions de boucle qui
+  permettent de réduire le domaine abstrait ? La définition précédente n'est
+  peut-être pas la bonne, car elle risque d'appliquer des élargissements que
+  l'on ne sait plus ensuite comment rétrécir pour refaire apparaître les
+  bonnes conditions. Cherchons une autre forme d'itération, par exemple :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+    s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|n>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>>
+  </eqnarray*>
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|a<rsub|n+1>>|<cell|\<in\>>|<cell|\<delta\><rsub|n>
+    <text| (choisi arbitrairement)>>>|<row|<cell|D<rsub|n+1><rsup|0>>|<cell|=>|<cell|lfp<rsub|r<rsub|a<rsub|n+1>><around*|(|s<rsub|n>|)>><around*|(|\<lambda\>i.r<rsub|a<rsub|n+1>><around*|(|s<rsub|n>\<sqcup\>g<rsup|#><around*|(|i|)>|)>|)>>>|<row|<cell|D<rsub|n+1>>|<cell|=>|<cell|D<rsub|n+1><rsup|0>\<sqcup\>g<rsup|#><around*|(|D<rsub|n+1><rsup|0>|)>>>|<row|<cell|s<rsub|n+1>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<rsub|n><around*|(|d|)>\<nabla\>D<rsub|n+1><around*|(|d|)>>|<cell|si
+    d\<in\>K<rsub|\<nabla\>,n> et d\<neq\>a<rsub|n+1>>>|<row|<cell|s<rsub|n><around*|(|d|)>\<sqcup\>D<rsub|n+1><around*|(|d|)>>|<cell|sinon>>>>>>>|<row|<cell|K<rsub|\<nabla\>,n+1>>|<cell|=>|<cell|K<rsub|\<nabla\>,n>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+    s<rsub|n><around*|(|d|)>\<neq\>\<bot\>\<wedge\>s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n>|}>>>|<row|<cell|\<delta\><rsub|n+1>>|<cell|=>|<cell|<around*|(|\<delta\><rsub|n>\\<around*|{|a<rsub|n+1>|}>|)>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\|s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n><around*|(|d|)>|}>>>>>
+  </eqnarray*>
+
+  Où le point fixe <math|D<rsub|n+1><rsup|0>> est calculé avec appel au
+  widening au besoin, et en faisant une ou des itérations décroissantes à la
+  fin. Intuitivement : on fait grossir un état au maximum, en cherchant son
+  point fixe en boucle sur lui-même. Ensuite seulement on s'occupe de savoir
+  ce qu'il peut propager aux autres états.
+
+  <subsection|Domaine à arbre de disjonctions>
+
+  Définition du domaines abstraits avec graphes de décision : on va écrire
+  ici une définition mathématique des opérateurs que l'on a implémenté. On
+  fait abstraction des problématiques de mémoisation et de partage des
+  sous-graphes, qui font tout l'intérêt de la technique d'un point de vue
+  pratique mais qui peuvent être considérés comme un traitement à part (ce
+  n'est rien de plus que de la mémoisation et du partage).
+
+  <paragraph|Variables et contraintes.>Il y a deux domaines de variables,
+  <math|\<bbb-X\><rsub|e>> pour les énumérés et <math|\<bbb-X\><rsub|n>> pour
+  les variables numériques. Il y a deux domaines pour les contraintes,
+  <math|\<bbb-E\><rsub|e>> les contraintes sur les énumérés (de la forme
+  <math|x\<equiv\>y> ou <math|x\<equiv\>v,v\<in\>\<bbb-V\><rsub|e>>) et
+  <math|\<bbb-E\><rsub|n>> les contraintes sur les variables numériques
+  (égalités ou inégalités).
+
+  <paragraph|Domaine numérique.>On note <math|D<rsub|n>> le domaine des
+  valeurs numériques et <math|\<sqcup\><rsub|n>>, <math|\<sqcap\><rsub|n>>,
+  <math|<around*|\<llbracket\>|\<cdummy\>|\<rrbracket\>><rsub|n>>,
+  <math|\<bot\><rsub|n>>, <math|\<top\><rsub|n>>,
+  <math|\<sqsubseteq\><rsub|n>>, <math|\<matheuler\><rsub|n>>,
+  <math|\<nabla\><rsub|n>> les éléments correspondants dans ce domaine. On
+  considère que <math|\<gamma\><rsub|n> :
+  D<rsub|n>\<rightarrow\>\<cal-P\><around*|(|\<bbb-X\><rsub|e>\<cup\>\<bbb-X\><rsub|n>\<rightarrow\>\<bbb-V\>|)>>
+  donne toutes les valuations possibles pour les variables de
+  <math|\<bbb-X\><rsub|e>>.
+
+  <paragraph|Les EDD.>On définit un ordre sur les variables de
+  <math|\<bbb-X\><rsub|e>> : <math|\<bbb-X\><rsub|e>=<around*|{|x<rsub|1>,x<rsub|2>,\<ldots\>,x<rsub|n>|}>>
+  (bien choisi pour réduire la taille du graphe).
+
+  On définit ensuite une valeur du domaine disjonctif, ie un EDD, par un type
+  somme comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s>|<cell|\<assign\>>|<cell|V<around*|(|t\<in\>D<rsub|num>|)>>>|<row|<cell|>|<cell|\|>|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,v<rsub|2>\<rightarrow\>s<rsub|2>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>>>>>
+  </eqnarray*>
+
+  Si on voit ça comme un arbre, alors il faut que si un noeud
+  <math|C<around*|(|x<rsub|i>,\<ldots\>|)>> est ancêtre d'un noeud
+  <math|C<around*|(|x<rsub|j>,\<ldots\>|)>>, alors <math|i\<less\>j> (par
+  rapport à l'ordre donné sur <math|\<bbb-X\><rsub|e>>).\ 
+
+  Pour faciliter les notations, on introduit le rang d'un noeud :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<delta\><around*|(|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|=>|<cell|i>>|<row|<cell|\<delta\><around*|(|V<around*|(|t|)>|)>>|<cell|=>|<cell|\<infty\>>>>>
+  </eqnarray*>
+
+  La contrainte se traduit par, pour tout noeud
+  <math|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>>,
+  on a <math|\<forall\>j,i\<less\>\<delta\><around*|(|s<rsub|j>|)>>.
+
+  On définit aussi la contrainte suivante : on n'a pas le droit d'avoir de
+  noeud <math|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,v<rsub|2>\<rightarrow\>s<rsub|2>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>>
+  si <math|s<rsub|1>=s<rsub|2>=*\<cdots\>*=s<rsub|p>>. Cela implique
+  l'unicité de l'arbre qui représente un environnement donné.
+
+  La concrétisation est définie comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<gamma\><around*|(|V<around*|(|t|)>|)>>|<cell|=>|<cell|\<gamma\><rsub|n><around*|(|t|)>>>|<row|<cell|\<gamma\><around*|(|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|=>|<cell|<big|cup><rsub|j=1><rsup|p><around*|{|s\<in\>\<gamma\><around*|(|s<rsub|j>|)>
+    \| s<around*|(|x<rsub|i>|)>=v<rsub|j>|}>>>>>
+  </eqnarray*>
+
+  Les éléments <math|\<top\>> et <math|\<bot\>> sont définis comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<top\>>|<cell|=>|<cell|V<around*|(|\<top\><rsub|n>|)>>>|<row|<cell|\<bot\>>|<cell|=>|<cell|V<around*|(|\<bot\><rsub|n>|)>>>>>
+  </eqnarray*>
+
+  Pour assurer l'unicité lors des transformations, on définit la fonction de
+  réduction <math|r> :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|r<around*|(|<around*|\<nobracket\>|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|\<nobracket\>>>|<cell|=>|<cell|<choice|<tformat|<table|<row|<cell|s<rsub|1>>|<cell|si
+    s<rsub|1>=s<rsub|2>=*\<cdots\>*s<rsub|p>>>|<row|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>>|<cell|sinon>>>>>>>>>
+  </eqnarray*>
+
+  L'opération <math|\<sqcap\>> est définie comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|V<around*|(|t|)>\<sqcap\>V<around*|(|t<rprime|'>|)>>|<cell|=>|<cell|V<around*|(|t\<sqcap\><rsub|n>t<rprime|'>|)>>>|<row|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>\<sqcap\>C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1><rprime|'>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p><rprime|'>|)>>|<cell|=>|<cell|r<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>\<sqcap\>s<rsub|1><rprime|'>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>\<sqcap\>s<rsub|p><rprime|'>|)>>>|<row|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>\<sqcap\>s<rprime|'>>|<cell|<above|=|<text|lorsque
+    <math|i\<less\>\<delta\><around*|(|s<rprime|'>|)>>>>>|<cell|<stack|<tformat|<table|<row|<cell|r<around*|(|<around*|\<nobracket\>|x<rsub|i>,<stack|<tformat|<table|<row|<cell|v<rsub|1>\<rightarrow\>s<rsub|1>\<sqcap\>s<rprime|'>>>|<row|<cell|*\<vdots\>>>|<row|<cell|v<rsub|p>\<rightarrow\>s<rsub|p>\<sqcap\>s<rprime|'>>>>>>|)>|\<nobracket\>>>>>>>>>>>
+  </eqnarray*>
+
+  et symmétriquement lorsque <math|\<delta\><around*|(|s|)>\<gtr\>\<delta\><around*|(|s<rprime|'>|)>>
+  (le noeud le plus haut est celui correspondant à la variable d'indice le
+  plus faible, pour respecter l'ordre).
+
+  L'opération <math|\<sqcup\>> est définie pareil.
+
+  Si <math|e\<in\>\<bbb-E\><rsub|n>>, on définit
+  <math|<around*|\<llbracket\>|e|\<rrbracket\>>> par :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|<around*|\<llbracket\>|e|\<rrbracket\>><around*|(|V<around*|(|t|)>|)>>|<cell|=>|<cell|V<around*|(|<around*|\<llbracket\>|e|\<rrbracket\>><rsub|n><around*|(|t|)>|)>>>|<row|<cell|<around*|\<llbracket\>|e|\<rrbracket\>><around*|(|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|=>|<cell|r<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\><around*|\<llbracket\>|e|\<rrbracket\>><around*|(|s<rsub|1>|)>,\<ldots\>,v<rsub|p>\<rightarrow\><around*|\<llbracket\>|e|\<rrbracket\>><around*|(|s<rsub|p>|)>|)>>>>>
+  </eqnarray*>
+
+  Pour les conditions sur les énumérés, on définit d'abord :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|c<around*|(|x\<equiv\>v|)>>|<cell|=>|<cell|C<around*|(|x,v\<rightarrow\>V<around*|(|\<top\>|)>,v<rprime|'>\<rightarrow\>V<around*|(|\<bot\>|)>,v<rprime|'>\<in\>\<bbb-V\><rsub|e>\\<around*|{|v|}>|)>>>|<row|<cell|c<around*|(|x\<nequiv\>v|)>>|<cell|=>|<cell|C<around*|(|x,v\<rightarrow\>V<around*|(|\<bot\>|)>,v<rprime|'>\<rightarrow\>V<around*|(|\<top\>|)>,v<rprime|'>\<in\>\<bbb-V\><rsub|e>\\<around*|{|v|}>|)>>>|<row|<cell|c<around*|(|x<rsub|i>\<equiv\>x<rsub|j>|)>>|<cell|<above|=|lorsque
+    i\<less\>j>>|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>c<around*|(|x<rsub|j>\<equiv\>v<rsub|1>|)>,\<ldots\>,v<rsub|p>\<rightarrow\>c<around*|(|x<rsub|j>\<equiv\>v<rsub|p>|)>|)>>>|<row|<cell|c<around*|(|x<rsub|i>\<nequiv\>x<rsub|j>|)>>|<cell|<above|=|lorsque
+    i\<less\>j>>|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>c<around*|(|x<rsub|j>\<nequiv\>v<rsub|1>|)>,\<ldots\>,v<rsub|p>\<rightarrow\>c<around*|(|x<rsub|j>\<nequiv\>v<rsub|p>|)>|)>>>>>
+  </eqnarray*>
+
+  et symmétriquement lorsque <math|j\<gtr\>i>.
+
+  On peut ensuite poser :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|<around*|\<llbracket\>|e|\<rrbracket\>><around*|(|s|)>>|<cell|=>|<cell|c<around*|(|e|)>\<sqcap\>s>>>>
+  </eqnarray*>
+
+  L'égalité entre les valeurs représentées par deux EDD correspond à
+  l'égalité de ces deux EDD (c'est une CNS).
+
+  L'inclusion est également définie par induction :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|V<around*|(|t|)>\<sqsubseteq\>V<around*|(|t<rprime|'>|)>>|<cell|\<equiv\>>|<cell|t\<sqsubseteq\><rsub|n>t<rprime|'>>>|<row|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>\<sqsubseteq\>C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1><rprime|'>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p><rprime|'>|)>>|<cell|\<equiv\>>|<cell|<big|wedge><rsub|i=1><rsup|p>s<rsub|i>\<sqsubseteq\>s<rsub|i><rprime|'>>>|<row|<cell|s\<sqsubseteq\>C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,v<rsub|2>\<rightarrow\>s<rsub|2>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>>|<cell|<above|\<equiv\>|lorsque
+    \<delta\><around*|(|s|)>\<gtr\>i>>|<cell|<big|wedge><rsub|i=1><rsup|p>s\<sqsubseteq\>s<rsub|i>>>|<row|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,v<rsub|2>\<rightarrow\>s<rsub|2>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>\<sqsubseteq\>s<rprime|'>>|<cell|<above|\<equiv\>|lorsque
+    i\<less\>\<delta\><around*|(|s<rprime|'>|)>>>|<cell|<big|wedge><rsub|i=1><rsup|p>s<rsub|i>\<sqsubseteq\>s<rprime|'>>>>>
+  </eqnarray*>
+
+  <paragraph|Opérateur de widening.>Sur nos EDD, on définit une opération
+  <math|\<rho\>:D<rsub|n>\<times\>D\<rightarrow\>D> comme suit :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<rho\><around*|(|t<rsub|0>,V<around*|(|t|)>|)>>|<cell|=>|<cell|<choice|<tformat|<table|<row|<cell|\<top\>>|<cell|si
+    t=t<rsub|0>>>|<row|<cell|\<bot\>>|<cell|sinon>>>>>>>|<row|<cell|\<rho\><around*|(|t<rsub|0>,C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|=>|<cell|r<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>\<rho\><around*|(|t<rsub|0>,s<rsub|1>|)>,\<ldots\>,v<rsub|p>\<rightarrow\>\<rho\><around*|(|t<rsub|0>,s<rsub|p>|)>|)>>>>>
+  </eqnarray*>
+
+  Explication : cette fonction extrait d'un EDD la fonction booléenne qui
+  mène vers exactement une certaine valeur abstraite des numériques.
+
+  On introduit maintenant un opérateur de widening sur nos arbres :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|a\<nabla\>b>|<cell|=>|<cell|f<rsub|\<nabla\>><around*|(|a,b,a,b|)>>>|<row|<cell|f<rsub|\<nabla\>><around*|(|a,b,V<around*|(|t|)>,V<around*|(|t<rprime|'>|)>|)>>|<cell|=>|<cell|<choice|<tformat|<table|<row|<cell|V<around*|(|t
+    \<nabla\><rsub|n>t<rprime|'>|)>>|<cell|si
+    \<rho\><around*|(|t,a|)>=\<rho\><around*|(|t<rprime|'>,b|)>>>|<row|<cell|V<around*|(|t\<sqcup\><rsub|n>t<rprime|'>|)>>|<cell|sinon>>>>>>>|<row|<cell|f<rsub|\<nabla\>><around*|(|a,b,s,C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|<above|=|lorsque
+    i\<less\>\<delta\><around*|(|s|)>>>|<cell|r<around*|(|x<rsub|i>,<stack|<tformat|<table|<row|<cell|v<rsub|1>\<rightarrow\>f<rsub|\<nabla\>><around*|(|a,b,s,s<rsub|1>|)>>>|<row|<cell|*\<vdots\>>>|<row|<cell|v<rsub|p>\<rightarrow\>f<rsub|\<nabla\>><around*|(|a,b,s,s<rsub|p>|)>>>>>>|)>>>>>
+  </eqnarray*>
+
+  Les autres cas sont définis exactement pareil (cf définition de
+  <math|\<sqcup\>>, plus on passe <math|a> et <math|b> à notre fonction
+  <math|f<rsub|\<nabla\>>>). Explication : lorsque l'on doit faire l'union de
+  deux feuilles, on fait un widening si et seulement si les deux feuilles
+  sont accessibles selont exactement la même formule booléenne sur les
+  énumérés dans <math|a> et <math|b>.
+
+  <paragraph|Itérations chaotiques.>On enrichit un peu notre arbre au niveau
+  des feuilles pour enregistrer quelques informations supplémentaires :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s>|<cell|\<assign\>>|<cell|V<around*|(|t|)><rsub|i>>>|<row|<cell|>|<cell|\|>|<cell|V<around*|(|t|)><rsub|i><rsup|\<ast\>>>>|<row|<cell|>|<cell|\|>|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,v<rsub|2>\<rightarrow\>s<rsub|2>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>>>>>
+  </eqnarray*>
+
+  L'étoile correspondra à : ``cette feuille est nouvelle, il faut l'analyse
+  comme nouveau cas'', et l'indice <math|i\<in\>\<bbb-N\>> correspond à :
+  ``cette feuille est là depuis <math|n> itérations'', où le <math|n> permet
+  d'implémenter un délai de widening.
+
+  On définit maintenant une fonction d'accumulation <math|\<diamond\>> comme
+  suit (<math|\<tau\>> correspond à un delai de widening) :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|a \<diamond\>
+    b>|<cell|=>|<cell|f<rsub|\<diamond\>><around*|(|a,b,a,b|)>>>|<row|<cell|f<rsub|\<diamond\>><around*|(|a,b,V<around*|(|\<bot\><rsub|n>|)><rsub|>,V<around*|(|t|)>|)>>|<cell|<above|=|lorsque
+    t\<neq\>\<bot\><rsub|n>>>|<cell|V<around*|(|t|)><rsub|0>>>|<row|<cell|f<rsub|\<diamond\>><around*|(|a,b,V<around*|(|t|)><rsub|i><rsup|\<nu\>>,V<around*|(|\<bot\><rsub|n>|)>|)>>|<cell|=>|<cell|V<around*|(|t|)><rsub|i><rsup|\<nu\>>>>|<row|<cell|f<rsub|\<diamond\>><around*|(|a,b,V<around*|(|t|)><rsub|i><rsup|\<nu\>>,V<around*|(|t<rprime|'>|)>|)>>|<cell|=>|<cell|<choice|<tformat|<table|<row|<cell|V<around*|(|t
+    \<nabla\><rsub|n>t<rprime|'>|)><rsub|i+1><rsup|\<nu\>>>|<cell|si
+    \<rho\><around*|(|t,a|)>=\<rho\><around*|(|t<rprime|'>,b|)>\<wedge\>
+    i\<geqslant\><rsub|>\<tau\>>>|<row|<cell|V<around*|(|t\<sqcup\><rsub|n>t<rprime|'>|)><rsub|i+1><rsup|\<nu\>>>|<cell|sinon>>>>>>>|<row|<cell|f<rsub|\<diamond\>><around*|(|a,b,s,C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|<above|=|lorsque
+    \<delta\><around*|(|s|)>\<gtr\>i>>|<cell|r<around*|(|x<rsub|i>,<stack|<tformat|<table|<row|<cell|v<rsub|1>\<rightarrow\>f<rsub|\<diamond\>><around*|(|a,b,s,s<rsub|1>|)>>>|<row|<cell|*\<vdots\>>>|<row|<cell|v<rsub|p>\<rightarrow\>f<rsub|\<diamond\>><around*|(|a,b,s,s<rsub|p>|)>>>>>>|)>>>>>
+  </eqnarray*>
+
+  (où <math|\<nu\>> correspond à soit une étoile soit pas d'étoile)
+
+  (les autres cas se font par appel récursif encore une fois comme dans le
+  cas de l'union)
+
+  Puis une fonction de détection des cas nouveaux par rapport à une valeur
+  précédente :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|\<oast\><rsub|s<rsub|0>><around*|(|s|)>>|<cell|=>|<cell|f<rsub|\<oast\>><around*|(|s<rsub|0>,s,s|)>>>|<row|<cell|f<rsub|\<oast\>><around*|(|s<rsub|0>,s,V<around*|(|t|)><rsub|i>|)>>|<cell|=>|<cell|<choice|<tformat|<table|<row|<cell|V<around*|(|t|)><rsub|i><rsup|\<ast\>>>|<cell|si
+    <around*|(|\<rho\><around*|(|t,s|)>\<sqcap\>s|)>\<nsqsubseteq\>s<rsub|0>>>|<row|<cell|V<around*|(|t|)><rsub|i>>|<cell|sinon>>>>>>>|<row|<cell|f<rsub|\<oast\>><around*|(|s<rsub|0>,s,V<around*|(|t|)><rsub|i><rsup|\<ast\>>|)>>|<cell|=>|<cell|V<around*|(|t|)><rsub|i><rsup|\<ast\>>>>|<row|<cell|f<rsub|\<oast\>><around*|(|s<rsub|0>,s,C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|=>|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>f<rsub|\<oast\>><around*|(|s<rsub|0>,s,s<rsub|1>|)><rsub|>,\<ldots\>,v<rsub|p>\<rightarrow\>f<rsub|\<oast\>><around*|(|s<rsub|0>,s,s<rsub|p>|)>|)>>>>>
+  </eqnarray*>
+
+  On commence avec :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|\<oast\><rsub|\<bot\>>
+    I<rsup|#>>>>>
+  </eqnarray*>
+
+  (appliquer <math|\<oast\>> de la sorte permet de faire que toutes les
+  feuilles soient étoilées)
+
+  Puis pour les<math|> itérations, deux cas :
+
+  <\itemize>
+    <item>Si il existe <math|V<around*|(|t<rsub|0>|)><rsup|\<ast\>><rsub|i>>
+    une feuille étoilée dans <math|s<rsub|n>> : on marque
+    <math|s<rsub|n><rprime|'>> l'arbre <math|s<rsub|n>> où toutes les
+    feuilles <math|V<around*|(|t<rsub|0>|)>> sont dé-étoilées, puis :
+
+    <\eqnarray*>
+      <tformat|<table|<row|<cell|c<rsub|n>>|<cell|=>|<cell|\<rho\><around*|(|t<rsub|0>,s<rsub|n>|)>>>|<row|<cell|D<rsub|n+1><rsup|0>>|<cell|=>|<cell|lfp<rsub|c<rsub|n>\<sqcap\>s<rsub|n>><around*|(|\<lambda\>i.c<rsub|n>\<sqcap\><around*|(|s<rsub|n>\<sqcup\>g<rsup|#><around*|(|i|)>|)>|)>>>|<row|<cell|D<rsub|n+1>>|<cell|=>|<cell|D<rsub|n+1><rsup|0>\<sqcup\>g<rsup|#><around*|(|D<rsub|n+1><rsup|0>|)>>>|<row|<cell|s<rsub|n+1>>|<cell|=>|<cell|\<oast\><rsub|s<rsub|n><rprime|'>><around*|(|s<rsub|n><rprime|'>
+      \<diamond\> D<rsub|n+1>|)>>>>>
+    </eqnarray*>
+
+    (où le point fixe <math|D<rsub|n+1><rsup|0>> est fait en faisant appel à
+    <math|\<sqcup\>> et <math|\<nabla\>> définis précédemment, avec un délai
+    de widening convenable)
+
+    Dans tous les cas, on refait une itération. Les étoiles finiront bien par
+    disparaitre.
+
+    <item>Si il n'existe pas de telle feuille étoilée dans <math|s<rsub|n>> :
+
+    <\eqnarray*>
+      <tformat|<table|<row|<cell|s<rsub|n+1>>|<cell|=>|<cell|\<oast\><rsub|s<rsub|n>><around*|(|s<rsub|n>
+      \<diamond\> g<rsup|#><around*|(|s<rsub|n>|)>|)>>>>>
+    </eqnarray*>
+
+    Dans ce cas, on s'arrête si <math|s<rsub|n+1>=s<rsub|n>>.
+  </itemize>
+</body>
+
+<\initial>
+  <\collection>
+    <associate|language|french>
+  </collection>
+</initial>
+
+<\references>
+  <\collection>
+    <associate|auto-1|<tuple|1|1>>
+    <associate|auto-10|<tuple|2.3.5|4>>
+    <associate|auto-11|<tuple|2.3.6|4>>
+    <associate|auto-12|<tuple|2.3.7|4>>
+    <associate|auto-13|<tuple|2.4|6>>
+    <associate|auto-14|<tuple|2.4.1|6>>
+    <associate|auto-15|<tuple|2.4.2|7>>
+    <associate|auto-16|<tuple|3|8>>
+    <associate|auto-17|<tuple|4|8>>
+    <associate|auto-18|<tuple|4.1|8>>
+    <associate|auto-19|<tuple|4.1.1|8>>
+    <associate|auto-2|<tuple|2|1>>
+    <associate|auto-20|<tuple|4.1.2|9>>
+    <associate|auto-21|<tuple|4.2|10>>
+    <associate|auto-22|<tuple|5|11>>
+    <associate|auto-23|<tuple|5.1|11>>
+    <associate|auto-24|<tuple|5.2|13>>
+    <associate|auto-25|<tuple|5.2.0.1|13>>
+    <associate|auto-26|<tuple|5.2.0.2|13>>
+    <associate|auto-27|<tuple|5.2.0.3|13>>
+    <associate|auto-28|<tuple|5.2.0.4|15>>
+    <associate|auto-29|<tuple|5.2.0.5|15>>
+    <associate|auto-3|<tuple|2.1|1>>
+    <associate|auto-4|<tuple|2.2|2>>
+    <associate|auto-5|<tuple|2.3|2>>
+    <associate|auto-6|<tuple|2.3.1|3>>
+    <associate|auto-7|<tuple|2.3.2|3>>
+    <associate|auto-8|<tuple|2.3.3|3>>
+    <associate|auto-9|<tuple|2.3.4|3>>
+  </collection>
+</references>
+
+<\auxiliary>
+  <\collection>
+    <\associate|toc>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-1><vspace|0.5fn>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|2<space|2spc>Spécification>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-2><vspace|0.5fn>
+
+      <with|par-left|<quote|1.5fn>|2.1<space|2spc>Grammaire
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-3>>
+
+      <with|par-left|<quote|1.5fn>|2.2<space|2spc>Sémantique concrète
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-4>>
+
+      <with|par-left|<quote|1.5fn>|2.3<space|2spc>Sémantique par réduction
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-5>>
+
+      <with|par-left|<quote|3fn>|2.3.1<space|2spc>Règles de réduction pour
+      l'activation du scope racine <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-6>>
+
+      <with|par-left|<quote|3fn>|2.3.2<space|2spc>Règles de réduction pour
+      l'init dans tous les scopes <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-7>>
+
+      <with|par-left|<quote|3fn>|2.3.3<space|2spc>Règles de réduction
+      d'expressions <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-8>>
+
+      <with|par-left|<quote|3fn>|2.3.4<space|2spc>Règles de réduction pour
+      les pre <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-9>>
+
+      <with|par-left|<quote|3fn>|2.3.5<space|2spc>Règles de réduction pour
+      les affectations <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-10>>
+
+      <with|par-left|<quote|3fn>|2.3.6<space|2spc>Règles de réduction pour
+      les blocs activate <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-11>>
+
+      <with|par-left|<quote|3fn>|2.3.7<space|2spc>Règles de réduction pour
+      les automates <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-12>>
+
+      <with|par-left|<quote|1.5fn>|2.4<space|2spc>Sémantique par traduction,
+      règles de traduction <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-13>>
+
+      <with|par-left|<quote|3fn>|2.4.1<space|2spc>Traduction des expressions
+      numériques et booléennes <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-14>>
+
+      <with|par-left|<quote|3fn>|2.4.2<space|2spc>Traduction de scopes et de
+      programmes <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-15>>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|3<space|2spc>Interprète
+      pour sémantique concrète> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-16><vspace|0.5fn>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|4<space|2spc>Interprétation
+      abstraite> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-17><vspace|0.5fn>
+
+      <with|par-left|<quote|1.5fn>|4.1<space|2spc>Sémantique collectrice
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-18>>
+
+      <with|par-left|<quote|3fn>|4.1.1<space|2spc>Nouvelle notation :
+      fonction de transition <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-19>>
+
+      <with|par-left|<quote|3fn>|4.1.2<space|2spc>Suppression des entrées,
+      sémantique collectrice <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-20>>
+
+      <with|par-left|<quote|1.5fn>|4.2<space|2spc>Généralités sur
+      l'interprétation abstraite <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-21>>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|5<space|2spc>Domaines
+      abstraits et disjonction de cas> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-22><vspace|0.5fn>
+
+      <with|par-left|<quote|1.5fn>|5.1<space|2spc>Domaine à disjonction
+      simple <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-23>>
+
+      <with|par-left|<quote|1.5fn>|5.2<space|2spc>Domaine à arbre de
+      disjonctions <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-24>>
+
+      <with|par-left|<quote|6fn>|Variables et contraintes.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-25><vspace|0.15fn>>
+
+      <with|par-left|<quote|6fn>|Domaine numérique.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-26><vspace|0.15fn>>
+
+      <with|par-left|<quote|6fn>|Les EDD.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-27><vspace|0.15fn>>
+
+      <with|par-left|<quote|6fn>|Opérateur de widening.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-28><vspace|0.15fn>>
+
+      <with|par-left|<quote|6fn>|Itérations chaotiques.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-29><vspace|0.15fn>>
+    </associate>
+  </collection>
+</auxiliary>
\ No newline at end of file