summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 18:05:47 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-15 18:05:47 +0200
commitf55d48487697c358b8d3a3fa9c90f3f61596ba53 (patch)
tree1558f34f18bacaa9f5127045cbe0f4aed4d64095
parent4e66de932b91e91e4cadd943ff8859d6f69f57e1 (diff)
downloadscade-analyzer-f55d48487697c358b8d3a3fa9c90f3f61596ba53.tar.gz
scade-analyzer-f55d48487697c358b8d3a3fa9c90f3f61596ba53.zip
Begin redaction of README.
-rw-r--r--readme.pdfbin0 -> 211011 bytes
-rw-r--r--readme.tm1560
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
Binary files differ
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