diff options
| -rw-r--r-- | readme.pdf | bin | 0 -> 211011 bytes | |||
| -rw-r--r-- | readme.tm | 1560 |
2 files changed, 1560 insertions, 0 deletions
diff --git a/readme.pdf b/readme.pdf Binary files differnew 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 |