diff options
Diffstat (limited to 'doc/readme.tm')
| -rw-r--r-- | doc/readme.tm | 1936 |
1 files changed, 1936 insertions, 0 deletions
diff --git a/doc/readme.tm b/doc/readme.tm new file mode 100644 index 0000000..8622a9a --- /dev/null +++ b/doc/readme.tm @@ -0,0 +1,1936 @@ +<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 (primitives <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 mettrons 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> + + Par la suite, nous ne considérons que des programmes SCADE bien typés. + + <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. + + Un scope <math|\<Sigma\>> correspond à un ensemble de définitions (de + variables, d'automates, ou de blocs activate), identifiés par un chemin. + Chaque scope dispose d'une horloge propre. 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|act<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|/>|)>=tt>, + 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. Pour chaque + <math|pre<rsub|i> e>, on introduit la variable <math|m<rsub|i>> qui + enregistre la valeur de <math|e> dans le cycle courant et qui sert de + mémoire pour le pre lors du cycle suivant. + + 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*|{|\<epsilon\>|}>>, la + valeur <math|\<epsilon\>> 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\>\<epsilon\>>. + + Les déductions de la forme <math|l\<Rightarrow\>s> signifient \S avec la + mémoire <math|l>, on peut déduire du système l'état (partiel) <math|s> \T. + Les déductions de la forme <math|l,s\<vDash\>e\<rightarrow\><rsub|\<Sigma\>><rsup|v>v> + signifient \S 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> \T (la flèche <math|\<rightarrow\><rsub|\<Sigma\>><rsup|v>> + correspond à une réduction par valeur dans le scope <math|\<Sigma\>>). + + On notera <math|\<Sigma\>\<Vdash\>x=e> pour signifier \S dans le scope + <math|\<Sigma\>> on a la définition <math|x=e> \T, de même pour les + définitions de blocs activate et d'automates. On notera + <math|\<Sigma\>\<Vdash\>pre<rsub|i> e> pour signifier que <math|pre<rsub|i> + e> apparaît dans le scope <math|\<Sigma\>>. + + <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\>tt|]><around*|[|nreset<rsub|/>\<assign\>ff|]>> + </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\>tt|]>> + </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\>>|)>=tt>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>ff|]>> + </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\>>|)>=ff>>>>>|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|/>|)>=tt> + + <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. On note + <math|\<odot\>> n'importe quel opérateur binaire : + <math|+,-,\<times\>,/,mod,\<less\>,\<gtr\>,\<leqslant\>,\<geqslant\>,=,\<neq\>,\<wedge\>,\<vee\>>. + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac||l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>c>,c\<in\>\<bbb-V\>>|<cell|>|<cell|<frac|s<around*|(|x|)>\<neq\>\<epsilon\>|l,s\<vDash\>x\<rightarrow\><rsup|v><rsub|\<Sigma\>>s<around*|(|x|)>>,x\<in\>\<bbb-X\>>>>> + </eqnarray*> + + <\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*> + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|s<around*|(|init<rsub|\<Sigma\>>|)>=tt>|<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>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|s<around*|(|init<rsub|\<Sigma\>>|)>=ff>|<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>>>>>> + </eqnarray*> + + <\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\>>|)>=tt>|<cell|>|<cell|l,s\<vDash\>e\<rightarrow\><rsup|v><rsub|\<Sigma\>>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|i>\<assign\>v|]>>,\<Sigma\>\<Vdash\>pre<rsub|i> + e + </equation*> + + <\equation*> + <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=ff>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|i>\<assign\>l<around*|(|m<rsub|i>|)>|]>>,\<Sigma\>\<Vdash\>pre<rsub|i> + e + </equation*> + + <\equation*> + \; + </equation*> + + <subsubsection|Règles de réduction pour les définitions de variables> + + Pour toute définition <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\>>|)>=tt>|<cell|>|<cell|l,s\<vDash\>e\<rightarrow\><rsup|v><rsub|\<Sigma\>>v>>>>>|l\<Rightarrow\>s<around*|[|x\<assign\>v|]>>,\<Sigma\>\<Vdash\>x=e + </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\>>|)>=ff>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>ff|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>ff|]>> + </equation*> + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=tt>|<cell|>|<cell|l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>tt>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>tt|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>ff|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=tt>|<cell|>|<cell|l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>ff>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>ff|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>tt|]>>>>>> + </eqnarray*> + + (implicitement sur toutes les règles : <math|\<Sigma\>\<Vdash\>activate if + c then b<rsub|1> else b<rsub|2>>) + + 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 se place dans le cadre <math|\<Sigma\>\<Vdash\>A>. On note + <math|s<rsub|0>> l'état initial de <math|A>. 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 : + + <\eqnarray*> + <tformat|<table|<row|<cell|<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>|]>>>|<cell|>|<cell|<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>|)>|]>>>>>> + </eqnarray*> + + 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 : + + <\eqnarray*> + <tformat|<table|<row|<cell|<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>>=tt|]>>>|<cell|>|<cell|<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>>=ff|]>>>>>> + </eqnarray*> + + 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 à <em|true> dès que l'on + emprunte une transition qui reset, et à <em|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>tt>>>>>|l\<Rightarrow\>s<around*|[|nstate<rsub|A>\<assign\>s<rsub|j>|]>> + </equation*> + + À cela, il faut rajouter les conditions qui disent que l'on emprunte + 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 : + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|l\<Rightarrow\>s|l\<Rightarrow\>s<around*|[|act<rsub|/>\<assign\>tt|]><around*|[|nreset<rsub|/>\<assign\>ff|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s + >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=tt>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|/>\<assign\>tt|]>>>>>> + </eqnarray*> + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s + >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=ff>|<cell|>|<cell|l<around*|(|act<rsub|/>|)>=tt>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|/>\<assign\>ff|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s + >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=ff>|<cell|>|<cell|l<around*|(|act<rsub|/>|)>=ff>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|/>\<assign\>l<around*|(|init<rsub|/>|)>|]>>>>>> + </eqnarray*> + + Définition <verbatim|c = a - b> (la réduction par valeur de <math|a-b> en + une valeur <math|v> se fait selon les règles données ci-dessus) : + + <\equation*> + <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<cell|>|<cell|l,s\<vDash\>a-b\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|c\<assign\>v|]>> + </equation*> + + Définitions de <verbatim|la<math|>> et <verbatim|lb> : + + <\equation*> + <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<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|/>|)>=tt>|<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*> + + Définition de <verbatim|half> : + + <\equation*> + <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<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> (on écrit aussi les règles pour le cas où le scope + est inactif à titre d'exemple simplement ; en pratique celles-ci sont + éliminées puisque le scope racine est toujours actif) : + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<cell|>|<cell|l,s\<vDash\>a\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|1>\<assign\>v|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=ff>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|1>\<assign\>l<around*|(|m<rsub|1>|)>|]>>>>>> + </eqnarray*> + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<cell|>|<cell|l,s\<vDash\>b\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|2>\<assign\>v|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=ff>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|2>\<assign\>l<around*|(|m<rsub|2>|)>|]>>>>>> + </eqnarray*> + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|3>\<assign\>v|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=ff>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|3>\<assign\>l<around*|(|m<rsub|3>|)>|]>>>>>> + </eqnarray*> + + Activation des deux moitiés du activate : + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\>tt>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=tt|]><around*|[|act<rsub|/2>\<assign\>ff|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=tt>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\>ff>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=ff|]><around*|[|act<rsub|/2>\<assign\>tt|]>>>>>> + </eqnarray*> + + <\equation*> + <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=ff>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=ff|]><around*|[|act<rsub|/2>\<assign\>ff|]>> + </equation*> + + Définition de <verbatim|a> et <verbatim|b> dans la première moitié : + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/1>|)>=tt>|<cell|>|<cell|l,s\<vDash\>la+1\<rightarrow\><rsub|/1><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|a\<assign\>v|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/1>|)>=tt>|<cell|>|<cell|l,s\<vDash\>lb\<rightarrow\><rsub|/1><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|b\<assign\>v|]>>>>>> + </eqnarray*> + + Et dans la deuxième moitié : + + <\eqnarray*> + <tformat|<table|<row|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/2>|)>=tt>|<cell|>|<cell|l,s\<vDash\>la\<rightarrow\><rsub|/2><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|a\<assign\>v|]>>>|<cell|>|<cell|<frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/2>|)>=tt>|<cell|>|<cell|l,s\<vDash\>lb+1\<rightarrow\><rsub|/2><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|b\<assign\>v|]>>>>>> + </eqnarray*> + + 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 formule à 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 + être une formule booléenne. + + 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|T<around*|(|\<Sigma\>,e<rsub|1>,\<lambda\>f<rsub|1>.T<around*|(|\<Sigma\>,<around*|(|e<rsub|2>,\<ldots\>,e<rsub|n>|)>,w<around*|[|f<rsub|1>,\<box\><rsub|1>,\<ldots\>,\<box\><rsub|n-1>|]>|)>|)>>>|<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<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|2>,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, on définira la fonction de traduction d'une définition par : + + <\eqnarray*> + <tformat|<table|<row|<cell|T<rsub|def><around*|(|\<Sigma\>,x=e|)>>|<cell|=>|<cell|T<around*|(|\<Sigma\>,e,s<around*|(|x|)>=\<box\>|)>>>>> + </eqnarray*> + + Dans le cas d'une multi-affectation <math|x<rsub|1>,\<ldots\>,x<rsub|n>=e>, + on utilisera la traduction suivante : + + <\eqnarray*> + <tformat|<table|<row|<cell|T<rsub|def><around*|(|\<Sigma\>,<around*|(|x<rsub|1>,\<ldots\>,x<rsub|n>=e|)>|)>>|<cell|=>|<cell|T<around*|(|\<Sigma\>,e,s<around*|(|x<rsub|1>|)>=\<box\><rsub|1>\<wedge\>*\<cdots\>*\<wedge\>s<around*|(|x<rsub|n>|)>=\<box\><rsub|n>|)>>>>> + </eqnarray*> + + Dans le cas où l'on doit traduire une instanciation de noeud + <math|n<rsub|i><around*|(|v<rsub|1>,\<ldots\>,v<rsub|m>|)>> (c'est le cas + dans notre implémentation puisqu'on ne fait pas d'inlining), on nomme + <math|r<rsub|1>,\<ldots\>,r<rsub|n>> les valeurs renvoyées par le noeud et + on utilise la règle <math|T<around*|(|\<Sigma\>,n<rsub|i><around*|(|v<rsub|1>,\<ldots\>,v<rsub|m>|)>,w|)>=w<around*|[|s<around*|(|r<rsub|1>|)>,\<ldots\>,s<around*|(|r<rsub|n>|)>|]>>. + Il faut par ailleurs générer la traduction des définitions données dans le + noeud et s'occuper de passer les arguments (nommés + <math|arg<rsub|1>,\<ldots\>,arg<rsub|m>>), en introduisant des équations du + type <math|T<around*|(|\<Sigma\>,v<rsub|i>,s<around*|(|arg<rsub|i>|)>=\<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,s<around*|(|x|)>=\<box\>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|T<around*|(|\<Sigma\>,y\<geqslant\>0,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,y,s<around*|(|x|)>=\<box\>|)>|)>\<vee\><around*|(|\<neg\>T<around*|(|\<Sigma\>,y\<geqslant\>0,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,-y,s<around*|(|x|)>=\<box\>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|y|)>\<geqslant\>0\<wedge\>s<around*|(|x|)>=s<around*|(|y|)>|)>\<vee\><around*|(|\<neg\><around*|(|s<around*|(|y|)>\<geqslant\>0|)>\<wedge\>s<around*|(|x|)>=-s<around*|(|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\>T<around*|(|\<Sigma\>,1,<around*|\<nobracket\>|s<around*|(|x|)>=l<around*|(|m<rsub|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\>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 \S <math|activate if c then + b<rsub|1> else b<rsub|2>> \T 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 ceci 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. + + 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 + à appeler pour que cette valeur soit calculée et rajoutée à <math|s>. + + La procédure de calcul consiste à activer le scope racine, puis à appeler + 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 définition de variable <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 renvoyé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 + renvoyé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> + + Le calcul de la valeur prise par une expression <math|e>, utilisée dans une + condition ou pour une définition de variable, peut faire appel à d'autres + variables du programme. À ce moment si une valeur a été mémorisée on + l'utilise, sinon on appelle la fonction de calcul pour cette variable. + Lorsque le calcul d'une variable est \S en cours \T, ce statut est + enregistré dans <math|s>, ce qui permet de détecter les cycles de + dépendances. + + 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> + + 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\><rsub|e>> l'ensemble des variables de type énumération et + <math|\<bbb-X\><rsub|n>> les variables de type numérique, de sorte que + <math|\<bbb-X\>=\<bbb-X\><rsub|e>\<cup\>\<bbb-X\><rsub|n>>. + + 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|/>|)>=tt|}>>>>> + </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 mémoires 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 + préfixe standard, \S <math|L> \T, qui indique que ce sont des variables de + type <em|last>, c'est-à-dire des copies de valeurs du cycle précédent. + + On note cette fonction de cycle <math|c : + \<bbb-M\>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>> ; 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 + répétée 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 quelles 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*|{|tt,ff|}>> qui nous dit si un + environnement est conforme à la spécification donnée par les directives + <verbatim|assume>. + + 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|/>|)>=tt|}>>>|<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|)>|)>=tt|}>>>>> + </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 polyè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 polyè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 équations (é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 disparaît 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. + + <\example> + Soit le programme suivant : + + <\verbatim> + node counter() returns(x: int) + + \ \ x = 0 -\<gtr\> (if pre x = 5 then 0 else pre x + 1) + </verbatim> + + Celui-ci est traduit par une formule du style : + + <\eqnarray*> + <tformat|<table|<row|<cell|>|<cell|>|<cell|init<rsub|/>\<equiv\>Lnreset<rsub|/>>>|<row|<cell|>|<cell|\<wedge\>>|<cell|nreset<rsub|/>\<equiv\>ff>>|<row|<cell|>|<cell|\<wedge\>>|<cell|<around*|(|<tabular|<tformat|<table|<row|<cell|>|<cell|<around*|(|init<rsub|/>\<equiv\>tt\<wedge\>x=0|)>>>|<row|<cell|\<vee\>>|<cell|<around*|(|init<rsub|/>\<equiv\>ff\<wedge\><around*|(|<tabular|<tformat|<table|<row|<cell|>|<cell|<around*|(|Lx=5\<wedge\>x=0|)>>>|<row|<cell|\<vee\>>|<cell|<around*|(|Lx\<neq\>5\<wedge\>x=Lx+1|)>>>>>>|)>|)>>>>>>|)>>>>> + </eqnarray*> + + Les deux variables qui ont besoin d'être perpétuées d'un cycle au suivant + sont <math|nreset<rsub|/>> et <math|x>, la fonction de cycle + <math|c<rsup|#>> est donc définie à partir de + <math|C=<around*|{|nreset<rsub|/>,x|}>>. + + La fonction <math|f<rsup|#>>, quant à elle, reflète directement la + structure de la formule : + + <\eqnarray*> + <tformat|<table|<row|<cell|f<rsup|#><around*|(|s|)>>|<cell|=>|<cell|<around*|\<llbracket\>|init<rsub|/>\<equiv\>Lnreset<rsub|/>|\<rrbracket\>>\<circ\><around*|\<llbracket\>|nreset<rsub|/>\<equiv\>ff|\<rrbracket\>><around*|(|<tabular|<tformat|<table|<row|<cell|>|<cell|<around*|\<llbracket\>|init<rsub|/>\<equiv\>tt|\<rrbracket\>>\<circ\><around*|\<llbracket\>|x=0|\<rrbracket\>><around*|(|s|)>>>|<row|<cell|\<sqcup\>>|<cell|<around*|\<llbracket\>|init<rsub|/>\<equiv\>ff|\<rrbracket\>><around*|(|<tabular|<tformat|<table|<row|<cell|>|<cell|<around*|\<llbracket\>|Lx=5|\<rrbracket\>>\<circ\><around*|\<llbracket\>|x=0|\<rrbracket\>><around*|(|s|)>>>|<row|<cell|\<sqcup\>>|<cell|<around*|\<llbracket\>|Lx\<neq\>5|\<rrbracket\>>\<circ\><around*|\<llbracket\>|x=Lx+1|\<rrbracket\>><around*|(|s|)>>>>>>|)>>>>>>|)>>>>> + </eqnarray*> + </example> + + 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|I<rsup|#>> 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\>, + mod,=,\<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 transformations 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 de façon exacte les valeurs d'énumérations ayant plus de + deux éléments (puisqu'on se restreint à une enveloppe convexe). + + <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 des 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 selon 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\>>> + avec <math|e\<in\>\<bbb-E\><rsub|e>>. + + <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 amené à 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|#><rsub|0>> 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|#><rsub|0>> représente une + abstraction de <math|\<bbb-M\><rsub|0>=<around*|(|\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>|)>\<rightarrow\>\<bbb-V\>>. + On note <math|\<bot\><rsub|0>> et <math|\<top\><rsub|0>> les éléments + bottom et top de ce treillis, <math|\<sqcup\><rsub|0>> et + <math|\<sqcap\><rsub|0>> les bornes inf et sup de ce treillis, ainsi que + <math|\<nabla\><rsub|0>> son opérateur de widening. On note + <math|<around*|\<llbracket\>|\<cdummy\>|\<rrbracket\>><rsub|0>> la fonction + de restriction par une contrainte. + + La particularité des variables de disjonction 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 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|)>=d<around*|(|x|)>|}>>. + De même on identifie <math|e\<in\>\<bbb-M\><rsub|0>> à + <math|<around*|{|s\<in\>\<bbb-M\> \| \<forall\>x\<in\>\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>,s<around*|(|x|)>=e<around*|(|x|)>|}>>. + + On construit maintenant le domaine abstrait disjonctif comme suit : + + <\eqnarray*> + <tformat|<table|<row|<cell|\<cal-D\><rsup|#>>|<cell|=>|<cell|\<bbb-M\><rsub|d>\<rightarrow\>\<cal-D\><rsup|#><rsub|0>>>|<row|<cell|\<gamma\><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\>>|<cell|=>|<cell|\<lambda\>d.\<bot\><rsub|0>>>|<row|<cell|\<top\><rsub|>>|<cell|=>|<cell|\<lambda\>d.\<top\><rsub|0>>>>> + </eqnarray*> + + On vérifie bien que <math|\<gamma\><around*|(|\<bot\>|)>=\<varnothing\>> et + <math|\<gamma\><around*|(|\<top\>|)>=\<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|0>t<around*|(|d|)>|)>>>|<row|<cell|s\<sqcap\>t>|<cell|=>|<cell|\<lambda\>d.<around*|(|s<around*|(|d|)>\<sqcap\><rsub|0>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\><rsup|#>>, + + <\eqnarray*> + <tformat|<table|<row|<cell|<around*|\<llbracket\>|x=y|\<rrbracket\>><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|0>>|<cell|sinon>>>>>>>|<row|<cell|<around*|\<llbracket\>|x\<neq\>y|\<rrbracket\>><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|0>>|<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\>><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si + d<around*|(|x|)>=v>>|<row|<cell|\<bot\><rsub|0>>|<cell|sinon>>>>>>>|<row|<cell|<around*|\<llbracket\>|x\<neq\>v|\<rrbracket\>><rsub|><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|0>>|<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 de + <math|\<bbb-V\><rsub|d>>. Pour toute expression + <math|e\<in\>\<bbb-E\><rsub|n>> ou <math|e\<in\>\<bbb-E\><rsub|e>>, le + domaine <math|\<cal-D\><rsup|#><rsub|0>> 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\>><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<around*|\<llbracket\>|e|\<rrbracket\>><rsub|0><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\> + t>|<cell|=>|<cell|\<lambda\>d.s<around*|(|d|)> \<nabla\><rsub|0> + 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\>><around*|(|\<top\>|)>>. + + Pour <math|d<rsub|0>\<in\>\<bbb-M\><rsub|d>>, notons + <math|r<rsub|d<rsub|0>> : \<cal-D\><rsup|#>\<rightarrow\>\<cal-D\><rsup|#>> + tel que <math|r<rsub|d<rsub|0>><around*|(|s|)>=\<lambda\>d.<choice|<tformat|<table|<row|<cell|\<bot\><rsub|0>>|<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 : + + <\itemize> + <item>Poser : + + <\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|0>|}>>>>> + </eqnarray*> + + <item>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*> + </itemize> + + 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 connaît. + + 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|0>|}>>>|<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\><rsub|0> D<rsub|n+1><around*|(|d|)>>|<cell|si + d\<in\>K<rsub|\<nabla\>,n>>>|<row|<cell|s<rsub|n><around*|(|d|)> + \<sqcup\><rsub|0> 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\><rsub|0>\<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. Nous proposons comme forme final le processus + d'itération suivant : + + <\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|0>|}>>>|<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\><rsub|0> 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\><rsub|0> 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\><rsub|0>\<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 à graphe de décision> + + Nous proposons dans ce paragraphe un second domaine abstrait capable de + faire des disjonctions de cas, et qui permet de mieux traîter des problèmes + ayant un nombre important de variables de type énuméré reliées entre elles + par des relations complexes. + + 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). + + <subsubsection|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). + + <subsubsection|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-M\>|)>> (avec + <math|\<bbb-M\>=\<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>>. + + <subsubsection|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|<stack|<tformat|<table|<row|<cell|>|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>>>|<row|<cell|\<sqcap\>>|<cell|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 symé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\>\<top\>,v<rprime|'>\<rightarrow\>\<bot\>,v<rprime|'>\<in\>\<bbb-V\><rsub|e>\\<around*|{|v|}>|)>>>|<row|<cell|c<around*|(|x\<nequiv\>v|)>>|<cell|=>|<cell|C<around*|(|x,v\<rightarrow\>\<bot\>,v<rprime|'>\<rightarrow\>\<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 symétriquement lorsque <math|j\<gtr\>i>. + + On peut ensuite poser, pour <math|e\<in\>\<bbb-E\><rsub|e>> : + + <\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*> + + <subsubsection|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 selon exactement la même formule booléenne sur les + énumérés dans <math|a> et <math|b>. + + <subsubsection|<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 à : \S cette feuille est nouvelle, il faut l'analyse + comme nouveau cas \T, et l'indice <math|i\<in\>\<bbb-N\>> correspond à : \S + cette feuille est là depuis <math|k> itérations \T, où le <math|k> permet + d'implémenter un délai de widening. + + On se donne <math|\<tau\>> un délai de widening, paramètre de l'analyse. On + définit maintenant une fonction d'accumulation <math|\<diamond\>> comme + suit : + + <\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,\<bot\><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\>>,\<bot\>|)>>|<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|)><text| et > + 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*> + + Nous sommes maintenant en mesure de décrire le processus d'itérations + chaotiques à proprement parler. 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 + disparaître. + + <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> + + <section|Partitionnement dynamique> + + Une autre approche à base de partitionnement dynamique a été tentée, mais + elle n'a pas donné de très bons résultats par manque d'une heuristique sur + les partitionnements à effectuer. Détails à venir. + + <section|Implémentation> + + Le projet scade-analyzer propose une implémentation simple des composants + suivants : + + <\itemize> + <item>parser, lexer, typeur pour notre sous-ensemble de SCADE (source des + fichiers dans <verbatim|frontend/>) + + <item>interprète pour la sémantique cocnrète + (<verbatim|interpret/interpret.ml>) + + <item>implémentation de la transformation d'un programme en formule + logique ; quelques simplifications sur les formules logiques + (<verbatim|abstract/formula.ml>, <verbatim|abstract/transform.ml>). + + <item>domaine numérique non-relationnel basé sur les intervalles ; + domaine relationnel basé sur la bibliothèque externe Apron + (<verbatim|abstract/num_domain.ml>, <verbatim|abstract/nonrelational.ml>, + <verbatim|abstract/apron_domain.ml>, ...) + + <item>deux domaines abstraits et analyseur statique correspondant + (<verbatim|abstract/abs_interp.ml>, <verbatim|abstract/abs_interp_edd.ml>) + </itemize> + + En nous basant sur les options de la ligne de commande, nous allons + maintenant décrire les différentes fonctionnalités. + + <subsection|Parsing et affichage de programmes SCADE> + + <\itemize> + <item><verbatim|--dump> : parse un fichier SCADE et le ré-affiche en + sortie + + <item><verbatim|--dump-rn> : parse un fichier SCADE et le ré-affiche en + sortie, après une étape de renommage qui consiste à rendre les noms + unique au sein d'un noeud. Cette passe est implémentée dans + <verbatim|frontend/rename.ml>. + </itemize> + + <subsection|Interprète SCADE> + + <\itemize> + <item><verbatim|--test> : execute le programme SCADE donné en argument, + avec l'interprète <verbatim|interpret/interpret.ml> basé sur la + sémantique à réduction. Le programme doit satisfaire la spécification + suivante : avoir un noeud <verbatim|test> qui servira de racine, ce noeud + devant prendre une unique entrée, <verbatim|i>, qui est un compteur + incrémenté à chaque cycle, et renvoyant trois entiers, <verbatim|a>, + <verbatim|b> et <verbatim|c> (qui seront affichés en sortie), ainsi qu'un + booleen <verbatim|exit> qui indiquera que l'interprète doit terminer. Cf + fichiers dans <verbatim|tests/source/*.scade> pour des exemples. + + <item><verbatim|--vtest> : pareil mais affiche plus de détails (tout le + contenu de la mémoire est affiché à chaque cycle). + </itemize> + + <subsection|Analyse statique par interprétation abstraite> + + <subsubsection|Domaine à disjonctions simples> + + Cette analyse est implémentée dans <verbatim|abstract/abs_interp.ml>. + + <paragraph|Modes d'analyse> + + <\itemize> + <item><verbatim|--ai-itv> : fait une passe d'analyse statique par + interprétation abstraite utilisant le domaine à disjonctions simples, et + en s'appuyant sur le domaine non-relationnel à base d'intervalles pour la + partie numérique + + <item><verbatim|--ai-rel> : de même mais utilise le domaine abstrait + relationnel basé sur Apron (polyèdres) pour la partie numérique + </itemize> + + <paragraph|Options de l'analyse> + + <\itemize> + <item><verbatim|--root \<less\>noeud\<gtr\>> : spécifie le noeud racine + dont on veut faire l'analyse (par défaut : <verbatim|test>) + + <item><verbatim|--ai-vci> : affiche des détails sur le contenu de + l'accumulateur à chaque itération + + <item><verbatim|--ai-vvci> : affiche encore plus de détails + + <item><verbatim|--ai-wd \<less\>n\<gtr\>> : définit un délai pour les + opérations de widening (par défaut 5) + + <item><verbatim|--disj \<less\>vars\<gtr\>> : variables à utiliser comme + variables de disjonction (par défaut : aucune) + + <item><verbatim|--no-time \<less\>scopes\<gtr\>> : donne un certain + nombre de scopes pour lesquels ne pas introduire de variable + <verbatim|time> (par défaut <verbatim|all>, c'est-à-dire que + <verbatim|time> n'est jamais introduite). Lorsqu'une variable + <verbatim|time> est introduite, on génère les équations qui font en sorte + que <verbatim|time> soit égal au numéro du cycle depuis le début de + l'exécution du programme. + + <item><verbatim|--init \<less\>scopes\<gtr\>> : donne un certain nombre + de scopes pour lesquels introduire une variable <verbatim|init> (par + défaut <verbatim|all>). Il est envisageable de remplacer la variable + <verbatim|init> de chaque scope par une variable <verbatim|time>, les + disjonctions de cas init/non init se feront alors selon la condition + <math|time=0> ou <math|time\<geqslant\>1>. En ne générant ni variable + <verbatim|time> ni variable <verbatim|init>, la disjonction n'est pas + faite. + </itemize> + + <subsubsection|Domaine à disjonction par graphe de décision> + + Cette analyse est implémentée dans <verbatim|abstract/abs_interp_edd.ml>. + + <paragraph|Modes d'analyse> + + <\itemize> + <item><verbatim|--ai-itv-edd> : fait une passe d'analyse statique + utilisant le domaine à base d'EDD et en utilisant les intervalles comme + domaine de valeurs numériques + + <item><verbatim|--ai-rel-edd> : de même mais utilise le domaine abstrait + relationnel basé sur Apron (polyèdres) pour la partie numérique + </itemize> + + <paragraph|Options de l'analyse> + + <\itemize> + <item><verbatim|--root> + + <item><verbatim|--ai-vci>, <verbatim|--ai-vvci> + + <item><verbatim|--ai-wd> + + <item><verbatim|--no-time>, <verbatim|--init> + + <item>Non implémenté : paramètre <verbatim|--disj> pouvant intervenir sur + le choix des variables à considérer dans le graphe de décision + (actuellement toutes sont nécessairement considérées). + </itemize> + + <subsubsection|Analyse par partitionnement dynamique> + + Une troisième forme d'analyse, basée sur un partitionnement dynamique de + <math|S<rsup|#>> a été tentée. Celle-ci n'a pas donné de très bons + résultats, mais nous indiquons néanmoins son existence ici. + L'implémentation existe dans <verbatim|abstract/abs_interp_dynpart.ml>. + + <paragraph|Modes d'analyse> + + <\itemize> + <item><verbatim|--ai-s-itv-dp> : analyse par partitionnement dynamique, + utilise un domaine simple non-relationnel pour les valeurs énumérées et + les intervalles pour la partie numérique + + <item><verbatim|--ai-edd-itv-dp> : analyse par partitionnement dynamique, + utilise des graphes de décision pour représenter les conditions sur les + énumérées et les intervalles pour la partie numérique + + <item><verbatim|--ai-s-rel-dp> + + <item><verbatim|--ai-edd-rel-dp> + </itemize> + + <paragraph|Paramètres de l'analyse> + + <\itemize> + <item><verbatim|--root> + + <item><verbatim|--ai-wd> + + <item><verbatim|--ai-vci>, <verbatim|--ai-vvci> + + <item><verbatim|--no-time>, <verbatim|--init> + + <item><verbatim|--ai-max-dp-depth> : profondeur maximale de + partitionnement + + <item><verbatim|--ai-max-dp-width> : largeur maximale de partitionnement + (ie nombre maximal de parties à considérer) + </itemize> + + <section|Prolongements envisageables> + + <subsection|Analyse des propriétés des nombres flottants> + + <\itemize> + <item>Implémenter un domaine d'intervalles permettant de gérer les + rationnels en précision arbitraire, ou se brancher sur le module Box + d'Apron + + <item>Utiliser un opérateur de widening aproprié (cf Astrée) + + <item>Implémenter la sémantique des nombres flottants machine (ce qui + n'est pas simple) + </itemize> + + <subsection|Analyse de programmes \S taille réelle \T> + + <\itemize> + <item>Modification du domaine EDD pour pouvoir ne prendre en compte + qu'une partie des variables énumérées (pour l'instant elles sont toutes + considérées, ce n'est pas paramétrable). Permettre que les feuilles + contiennent également des informations non-relationnelles sur les + variables de type énuméré. + + <item>Analyse de base avec des intervalles, plus des \S packs \T de + variables traités avec des domaines plus puissants (octagones, + polyhèdres, domaines à disjonctions) + + <item>Analyse par contrats : abstraire certains noeuds par les garanties + que vérifient les sorties, plutôt que de considérer le noeud en entrée. + En échange, il faut que l'on vérifie que les propriétés en entrée + (assume) sont bien vraies. + + <item>L'ordre des équations dans le programme semble avoir un impact sur + l'analyse : si celles-ci sont écrites dans l'ordre où elles seront + effectivement exécutées (ie triées par ordre de dépendance), l'analyse + semble gagner en précision. Implémenter une passe de scheduling + (approximatif : on ne veut pas diviser les automates, les blocs activate, + ...) que l'on exécuterait comme pré-processing sur le programme. + </itemize> + + <section|Références> + + <\itemize> + <item><name|N.Halbwachs>, <em|About synchronous programming and abstract + interpretation>, International Symposium on Static Analysis, SAS'94. + + <item><name|N.Halbwachs>, <name|F.Lagnier> and <name|C.Ratel>, + <em|Programming and verifying real-time systems by means of the + synchronous data-flow programming language Lustre>, IEEE Transactions on + Software Engineering, Spcial Issue on the Specification and Analysis of + Real-Time Systems, Sept. 1992 + + <item><name|B.Jeannet>, <name|N.Halbwachs> and <name|P.Raymond>, + <em|Dynamic Partitioning in Analyses of Numerical Properties>, Static + Analysis Symposium, SAS'99. + </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|7>> + <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|9>> + <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.1|14>> + <associate|auto-26|<tuple|5.2.2|14>> + <associate|auto-27|<tuple|5.2.3|14>> + <associate|auto-28|<tuple|5.2.4|15>> + <associate|auto-29|<tuple|5.2.5|16>> + <associate|auto-3|<tuple|2.1|1>> + <associate|auto-30|<tuple|5.2.3.3|?>> + <associate|auto-31|<tuple|5.2.5.2|16>> + <associate|auto-32|<tuple|6|16>> + <associate|auto-33|<tuple|7|?>> + <associate|auto-34|<tuple|7.1|?>> + <associate|auto-35|<tuple|7.2|?>> + <associate|auto-36|<tuple|7.3|?>> + <associate|auto-37|<tuple|7.3.1|?>> + <associate|auto-38|<tuple|7.3.1.1|?>> + <associate|auto-39|<tuple|7.3.1.2|?>> + <associate|auto-4|<tuple|2.2|2>> + <associate|auto-40|<tuple|7.3.2|?>> + <associate|auto-41|<tuple|7.3.2.1|?>> + <associate|auto-42|<tuple|7.3.2.2|?>> + <associate|auto-43|<tuple|7.3.3|?>> + <associate|auto-44|<tuple|7.3.3.1|?>> + <associate|auto-45|<tuple|7.3.3.2|?>> + <associate|auto-46|<tuple|8|?>> + <associate|auto-47|<tuple|8.1|?>> + <associate|auto-48|<tuple|8.2|?>> + <associate|auto-49|<tuple|9|?>> + <associate|auto-5|<tuple|2.3|3>> + <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|4>> + </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 définitions de variables <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 à graphe de + décision <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|3fn>|5.2.1<space|2spc>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>> + + <with|par-left|<quote|3fn>|5.2.2<space|2spc>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>> + + <with|par-left|<quote|3fn>|5.2.3<space|2spc>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>> + + <with|par-left|<quote|3fn>|5.2.4<space|2spc>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>> + + <with|par-left|<quote|3fn>|5.2.5<space|2spc><assign|paragraph-numbered|<quote|false>><assign|paragraph-prefix|<quote|<macro|<compound|the-paragraph>.>>><assign|paragraph-nr|<quote|1>><hidden|<tuple>><assign|subparagraph-nr|<quote|0>><flag|table + des matières|dark green|what><assign|auto-nr|<quote|30>><label|auto-30><write|toc|<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-30><vspace|0.15fn>>><no-indent><with|math-font-series|<quote|bold>|font-series|<quote|bold>|<vspace*|0.5fn>Itérations + chaotiques.<space|2spc>> <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-30>> + + <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-31><vspace|0.15fn>> + + <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Implémentation> + <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-32><vspace|0.5fn> + + <with|par-left|<quote|1.5fn>|6.1<space|2spc>Parsing et affichage de + programmes SCADE <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-33>> + + <with|par-left|<quote|1.5fn>|6.2<space|2spc>Interprète SCADE + <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-34>> + + <with|par-left|<quote|1.5fn>|6.3<space|2spc>Analyse statique par + 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-35>> + + <with|par-left|<quote|3fn>|6.3.1<space|2spc>Domaine à disjonctions + simples <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-36>> + + <with|par-left|<quote|6fn>|Modes d'analyse + <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-37><vspace|0.15fn>> + + <with|par-left|<quote|6fn>|Options de l'analyse + <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-38><vspace|0.15fn>> + + <with|par-left|<quote|3fn>|6.3.2<space|2spc>Domaine à disjonction par + graphe de décision <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-39>> + + <with|par-left|<quote|6fn>|Modes d'analyse + <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-40><vspace|0.15fn>> + + <with|par-left|<quote|6fn>|Options de l'analyse + <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-41><vspace|0.15fn>> + + <with|par-left|<quote|3fn>|6.3.3<space|2spc>Analyse par partitionnement + dynamique <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-42>> + + <with|par-left|<quote|6fn>|Modes d'analyse + <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-43><vspace|0.15fn>> + + <with|par-left|<quote|6fn>|Paramètres de l'analyse + <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-44><vspace|0.15fn>> + + <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Bibliographie> + <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-45><vspace|0.5fn> + </associate> + </collection> +</auxiliary>
\ No newline at end of file |