diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-23 18:03:28 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-23 18:03:28 +0200 |
| commit | 2073dd00710add906cc94099cd4bfb7aa3a2f85e (patch) | |
| tree | e4c3ff51a2283b9baa8f148e9b7446add9d99571 /readme.tm | |
| parent | 743f5cd5fb39e3ec58f94e43fe25ae8c25de7443 (diff) | |
| download | scade-analyzer-2073dd00710add906cc94099cd4bfb7aa3a2f85e.tar.gz scade-analyzer-2073dd00710add906cc94099cd4bfb7aa3a2f85e.zip | |
Move README && add stuff ; add presentation.
Diffstat (limited to 'readme.tm')
| -rw-r--r-- | readme.tm | 1813 |
1 files changed, 0 insertions, 1813 deletions
diff --git a/readme.tm b/readme.tm deleted file mode 100644 index 0d6388c..0000000 --- a/readme.tm +++ /dev/null @@ -1,1813 +0,0 @@ -<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|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> -</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|6.1|?>> - <associate|auto-34|<tuple|6.2|?>> - <associate|auto-35|<tuple|6.3|?>> - <associate|auto-36|<tuple|6.3.1|?>> - <associate|auto-37|<tuple|6.3.1.1|?>> - <associate|auto-38|<tuple|6.3.1.2|?>> - <associate|auto-39|<tuple|6.3.2|?>> - <associate|auto-4|<tuple|2.2|2>> - <associate|auto-40|<tuple|6.3.2.1|?>> - <associate|auto-41|<tuple|6.3.2.2|?>> - <associate|auto-42|<tuple|6.3.3|?>> - <associate|auto-43|<tuple|6.3.3.1|?>> - <associate|auto-44|<tuple|6.3.3.2|?>> - <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> - </associate> - </collection> -</auxiliary>
\ No newline at end of file |