diff options
| -rw-r--r-- | readme.pdf | bin | 211011 -> 221365 bytes | |||
| -rw-r--r-- | readme.tm | 686 |
2 files changed, 369 insertions, 317 deletions
| Binary files differ @@ -23,7 +23,7 @@ <\itemize> <item>noyau dataflow (opérations arithmétiques élémentaires, opérateurs <verbatim|-\<gtr\>> et <verbatim|pre>), pas de prise en charge des - horloges explicites (primitves <verbatim|when>, <verbatim|merge>, ...) + horloges explicites (primitives <verbatim|when>, <verbatim|merge>, ...) <item>blocs <verbatim|activate> @@ -32,7 +32,7 @@ prises en compte) </itemize> - Dans ce document nous metterons au clair les points suivants : + Dans ce document nous mettrons au clair les points suivants : <\enumerate> <item>Spécification du sous-ensemble de SCADE considéré @@ -57,6 +57,8 @@ </itemize> </enumerate> + Par la suite, nous ne considérons que des programmes SCADE bien typés. + <section|Spécification> <subsection|Grammaire> @@ -158,8 +160,11 @@ <math|i<rsub|n>>, il existe un unique état <math|s<rsub|n>> qui remplit la condition. - Pour traduire l'init et le reset, on introduit dans chaque scope - <math|\<Sigma\>> plusieurs variables : + 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 @@ -168,8 +173,8 @@ <item><math|init<rsub|\<Sigma\>>> : indique que le scope est à l'état initial dans ce cycle - <item><math|active<rsub|\<Sigma\>>> : indique qu'un scope est actif dans - ce cycle + <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 @@ -185,15 +190,15 @@ défini </itemize> - L'état <math|s<rsub|0>> est défini par <math|s<rsub|0><around*|(|reset<rsub|/>|)>=true>, + 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, et pour - chaque <math|pre<rsub|i> e>, on introduit la variable <math|m<rsub|i>> qui - enregistre la valeur de <math|e> dans l'état et qui sert de mémoire pour le - pre. + 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 @@ -203,20 +208,27 @@ <subsection|Sémantique par réduction> On définit notre ensemble d'environnements comme étant - <math|\<bbb-X\>\<rightarrow\>\<bbb-V\>\<cup\><around*|{|\<top\>|}>>, la - valeur <math|\<top\>> signifiant qu'une variable n'a pas encore pris sa + <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\>\<top\>>. + <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 ``avec la - mémoire <math|l>, on peut déduire du système l'état (partiel) <math|s>''. + Les déductions de la forme <math|l\<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 ``avec la mémoire <math|l> et l'état partiellement calculé + 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>''. + 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> @@ -227,7 +239,7 @@ toujours actif et jamais reset par la suite : <\equation*> - <frac|l\<Rightarrow\>s|l\<Rightarrow\>s<around*|[|act<rsub|/>\<assign\>t|]><around*|[|nreset<rsub|/>\<assign\>f|]>> + <frac|l\<Rightarrow\>s|l\<Rightarrow\>s<around*|[|act<rsub|/>\<assign\>tt|]><around*|[|nreset<rsub|/>\<assign\>ff|]>> </equation*> \; @@ -240,34 +252,32 @@ init ou pas : <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\>r<rsub|\<Sigma\>>>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>t|]>> + <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\>>|)>=t>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>f|]>> + <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\>>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>l<around*|(|init<rsub|\<Sigma\>>|)>|]>> + <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|/>|)>=t> + <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. - - <\equation*> - <frac||l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>c>,c\<in\>\<bbb-V\> - </equation*> + <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\>>. - <\equation*> - <frac|s<around*|(|x|)>\<neq\>\<top\>|l,s\<vDash\>x\<rightarrow\><rsup|v><rsub|\<Sigma\>>s<around*|(|x|)>>,x\<in\>\<bbb-X\> - </equation*> + <\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>|)>> @@ -277,13 +287,9 @@ <frac|<tabular|<tformat|<table|<row|<cell|l,s\<vDash\>e<rsub|1>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>>|<cell|>|<cell|l,s\<vDash\>e<rsub|2>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|2>>>>>>|l,s\<vDash\>e<rsub|1>\<odot\>e<rsub|2>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>\<odot\>v<rsub|2>> </equation*> - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|s<around*|(|init<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>e<rsub|1>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>>>>>>|l,s\<vDash\><around*|(|e<rsub|1>\<rightarrow\>e<rsub|2>|)>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|1>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|s<around*|(|init<rsub|\<Sigma\>>|)>=f>|<cell|>|<cell|l,s\<vDash\>e<rsub|2>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|2>>>>>>|l,s\<vDash\><around*|(|e<rsub|1>\<rightarrow\>e<rsub|2>|)>\<rightarrow\><rsup|v><rsub|\<Sigma\>>v<rsub|2>> - </equation*> + <\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\> @@ -295,20 +301,26 @@ <math|\<Sigma\>>, on donne les deux règles suivante : <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>e\<rightarrow\><rsup|v><rsub|\<Sigma\>>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|i>\<assign\>v|]>> + <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\>>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|i>\<assign\>l<around*|(|m<rsub|i>|)>|]>> + <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*> - <subsubsection|Règles de réduction pour les affectations> + <\equation*> + \; + </equation*> - Pour toute affectation <math|x=e> apparaissant dans le scope + <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\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>e\<rightarrow\><rsup|v><rsub|\<Sigma\>>v>>>>>|l\<Rightarrow\>s<around*|[|x\<assign\>v|]>> + <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> @@ -322,60 +334,52 @@ <math|\<Sigma\><rsub|2>> : <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>f|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>f|]>> + <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*> - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>t>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>t|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>f|]>> - </equation*> + <\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*> - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|\<Sigma\>>|)>=t>|<cell|>|<cell|l,s\<vDash\>c\<rightarrow\><rsup|v><rsub|\<Sigma\>>f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|1>>\<assign\>f|]><around*|[|act<rsub|\<Sigma\><rsub|2>>\<assign\>t|]>> - </equation*> + (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 note <math|A> l'automate, <math|s<rsub|0>> son état initial. Les règles - d'activation des différents scopes des états se font en fonction de la - variable <math|state<rsub|A>> définie pour l'automate <math|A> comme suit : - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\>r<rsub|\<Sigma\>>>>>>>|l\<Rightarrow\>s<around*|[|state<rsub|A>=s<rsub|0>|]>> - </equation*> + 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 : - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|l,s\<vDash\>\<neg\>r<rsub|\<Sigma\>>>>>>>|l\<Rightarrow\>s<around*|[|state<rsub|A>=l<around*|(|nstate<rsub|A>|)>|]>> - </equation*> + <\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 : - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|state<rsub|A>|)>=s<rsub|i>>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|i>>=t|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|state<rsub|A>|)>\<neq\>s<rsub|i>>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|\<Sigma\><rsub|i>>=f|]>> - </equation*> + <\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 à true dès que l'on emprunte - une transition qui reset, et à false le reste du temps. + <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>t>>>>>|l\<Rightarrow\>s<around*|[|nstate<rsub|A>\<assign\>s<rsub|j>|]>> + <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 emprune + À 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>>>. @@ -428,110 +432,81 @@ Initialisation : - <\equation*> - <frac|l\<Rightarrow\>s|l\<Rightarrow\>s<around*|[|act<rsub|/>\<assign\>t|]><around*|[|nreset<rsub|/>\<assign\>f|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s - >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=t>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|\<Sigma\>>\<assign\>t|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s - >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=f>|<cell|>|<cell|l<around*|(|act<rsub|/>|)>=t>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|/>\<assign\>f|]>> - </equation*> + <\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*> - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s - >|<cell|>|<cell|l<around*|(|nreset<rsub|/>|)>=f>|<cell|>|<cell|l<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|init<rsub|/>\<assign\>l<around*|(|init<rsub|/>|)>|]>> - </equation*> + <\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*> - Affectation <verbatim|c = a - b> : + 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|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>a-b\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|c\<assign\>v|]>> + <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*> - Affectations de <verbatim|la<math|>> et <verbatim|lb> : + 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|/>|)>=t>|<cell|>|<cell|l,s\<vDash\><around*|(|0\<rightarrow\>pre<rsub|1>|)> + <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|/>|)>=t>|<cell|>|<cell|l,s\<vDash\><around*|(|0\<rightarrow\>pre<rsub|2> + <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*> - Affectation de <verbatim|half> : + Définition de <verbatim|half> : <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\><around*|(|true\<rightarrow\>not + <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> : + <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) : - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>a\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|1>\<assign\>v|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>b\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|2>\<assign\>v|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\><rsub|/><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|3>\<assign\>v|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|1>\<assign\>l<around*|(|m<rsub|1>|)>|]>> - </equation*> + <\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*> - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|2>\<assign\>l<around*|(|m<rsub|2>|)>|]>> - </equation*> + <\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*> - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|m<rsub|3>\<assign\>l<around*|(|m<rsub|3>|)>|]>> - </equation*> + <\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 : - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\>t>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=t|]><around*|[|act<rsub|/2>\<assign\>f|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/>|)>=t>|<cell|>|<cell|l,s\<vDash\>half\<rightarrow\>f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=f|]><around*|[|act<rsub|/2>\<assign\>t|]>> - </equation*> + <\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|/>|)>=f>>>>>|l\<Rightarrow\>s<around*|[|act<rsub|/1>:=f|]><around*|[|act<rsub|/2>\<assign\>f|]>> + <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*> - Affectation de <verbatim|a> et <verbatim|b> dans la première moitié : + Définition de <verbatim|a> et <verbatim|b> dans la première moitié : - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/1>|)>=t>|<cell|>|<cell|l,s\<vDash\>la+1\<rightarrow\><rsub|/1><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|a\<assign\>v|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/1>|)>=t>|<cell|>|<cell|l,s\<vDash\>lb\<rightarrow\><rsub|/1><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|b\<assign\>v|]>> - </equation*> + <\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é : - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/2>|)>=t>|<cell|>|<cell|l,s\<vDash\>la\<rightarrow\><rsub|/2><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|a\<assign\>v|]>> - </equation*> - - <\equation*> - <frac|<tabular|<tformat|<table|<row|<cell|l\<Rightarrow\>s>|<cell|>|<cell|s<around*|(|act<rsub|/2>|)>=t>|<cell|>|<cell|l,s\<vDash\>lb+1\<rightarrow\><rsub|/2><rsup|v>v>>>>>|l\<Rightarrow\>s<around*|[|b\<assign\>v|]>> - </equation*> + <\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> @@ -549,7 +524,7 @@ On utilise des formules ``à trous'' pour faire la traduction. Un trou <math|\<box\>> correspond à la fonction <math|e\<mapsto\>e>, une formule <math|a\<wedge\>x=\<box\>> correspond à la fonction - <math|e\<mapsto\>a\<wedge\>x=e>, etc. L'argument d'une fonction trou peut + <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>. @@ -559,23 +534,40 @@ <math|\<Sigma\>> et devant être placée dans le trou <math|w>. En pratique, on divise <math|T> en deux fonctions, une pour les expressions booléennes et une pour les expressions numériques. Le résultat d'une traduction doit - généralement être une formule booléenne. - - On note <math|\<odot\>> n'importe quel opérateur binaire : - <math|+,-,\<times\>,/,mod,\<less\>,\<gtr\>,\<leqslant\>,\<geqslant\>,=,\<neq\>,\<wedge\>,\<vee\>>. + ê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|w<around*|[|T<rsub|><around*|(|\<Sigma\>,e<rsub|1>,\<box\>|)>,\<ldots\>,T<rsub|><around*|(|\<Sigma\>,e<rsub|n>,\<box\>|)>|]>>>|<row|<cell|\<forall\>c\<in\>\<bbb-V\>,<text| + <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<rsub|n><around*|(|\<Sigma\>,<around*|(|e<rsub|1>,e<rsub|2>|)>,w<around*|[|\<box\><rsub|1>\<odot\>\<box\><rsub|2>|]>|)>>>|<row|<cell|T<around*|(|\<Sigma\>,if - c then e<rsub|1> else e<rsub|2>,w|)>>|<cell|=>|<cell|<around*|(|T<around*|(|\<Sigma\>,c,\<box\>|)>\<wedge\>T<rsub|><around*|(|\<Sigma\>,e<rsub|1>,w|)>|)>\<vee\><around*|(|\<neg\>T<around*|(|\<Sigma\>,c,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,e<rsub|1>,w|)>|)>>>|<row|<cell|T<around*|(|\<Sigma\>,-e,w|)>>|<cell|=>|<cell|T<rsub|><around*|(|\<Sigma\>,e,w<around*|[|-\<box\>|]>|)>>>|<row|<cell|T<around*|(|\<Sigma\>,\<neg\>e,w|)>>|<cell|=>|<cell|T<rsub|><around*|(|\<Sigma\>,e,w<around*|[|\<neg\>\<box\>|]>|)>>>>> + 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*> - Par la suite, une affectation <math|x=e> sera traduite par la formule - booléenne <math|T<around*|(|\<Sigma\>,e,x=\<box\>|)>>. + 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 @@ -583,7 +575,7 @@ <\eqnarray*> <tformat|<table|<row|<cell|F>|<cell|=>|<cell|T<around*|(|\<Sigma\>,if - y\<geqslant\>0 then y else -y,x=\<box\>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|T<around*|(|\<Sigma\>,y\<geqslant\>0,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,y,x=\<box\>|)>|)>\<vee\><around*|(|\<neg\>T<around*|(|\<Sigma\>,y\<geqslant\>0,\<box\>|)>\<wedge\>T<around*|(|\<Sigma\>,-y,x=\<box\>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|y\<geqslant\>0\<wedge\>x=y|)>\<vee\><around*|(|\<neg\><around*|(|y\<geqslant\>0|)>\<wedge\>x=-y|)>>>>> + 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> @@ -593,12 +585,12 @@ <\eqnarray*> <tformat|<table|<row|<cell|F>|<cell|=>|<cell|T<around*|(|\<Sigma\>,0\<rightarrow\>pre<rsub|1>x + 1,s<around*|(|x|)>=\<box\>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,0,s<around*|(|x|)>=\<box\>|)>|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,pre<rsub|1>x - + 1,s<around*|(|x|)>=\<box\>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>T<around*|(|\<Sigma\>,<around*|(|pre<rsub|1>x,1|)>,s<around*|(|x|)>=\<box\><rsub|1>+\<box\><rsub|2>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\><around*|(|s<around*|(|x|)>=\<box\><rsub|1>+\<box\><rsub|2>|)><around*|(|T<around*|(|\<Sigma\>,pre<rsub|1>x,\<box\>|)>,T<around*|(|\<Sigma\>,1,\<box\>|)>|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\><around*|(|s<around*|(|x|)>=\<box\><rsub|1>+\<box\><rsub|2>|)><around*|(|l<around*|(|m<rsub|1>|)>,1|)>|)>>>|<row|<cell|>|<cell|=>|<cell|<around*|(|s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=0|)>\<vee\><around*|(|\<neg\>s<around*|(|init<rsub|\<Sigma\>>|)>\<wedge\>s<around*|(|x|)>=l<around*|(|m<rsub|1>|)>+1|)>>>>> + + 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|)>> + <math|s<around*|(|m<rsub|1>|)>=s<around*|(|x|)>>. </example> <subsubsection|Traduction de scopes et de programmes> @@ -611,11 +603,11 @@ activate). De manière générale, un scope a deux traductions qui sont produites : une pour le cas où ce scope est actif, et une pour le cas où il est inactif (dans le cas inactif, il s'agit simplement de perpétuer les - mémoires). Ainsi la traduction d'un bloc ``<math|activate if c then - b<rsub|1> else b<rsub|2>>'' sera du style + 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 cela est long à écrire, aussi nous nous contenterons de donner un + Tout ceci est long à écrire, aussi nous nous contenterons de donner un exemples. <\example> @@ -653,16 +645,15 @@ fixe. Ce n'est cependant pas cette solution que nous avons choisi de mettre en - place, notre solution est plus proche de la sémantique par réduction - définie plus haut. + 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 - à appeller pour que cette valeur soit calculée et rajoutée à <math|s>. + à appeler pour que cette valeur soit calculée et rajoutée à <math|s>. - La procédure de calcul consiste à activer le scope racine, puis à appeller + 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. @@ -670,20 +661,28 @@ L'activation d'un scope se fait selon la procédure suivante : <\itemize> - <item>Pour une affectation <math|x=e>, rajouter dans <math|s> pour la - variable <math|x> la fonction qui calcule <math|e> et rajoute la valeur - trouvée dans <math|s>. + <item>Pour 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 returnées par le bloc, la fonction qui choisit la branche à + 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 - returnées par l'automate, la fonction qui choisit l'état à activer en se + 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 @@ -693,15 +692,6 @@ <section|Interprétation abstraite> - \; - - <underline|<verbatim|/!\\>> <strong|travaux travaux travaux> - <verbatim|<underline|/!\\>> - - \; - - \; - Le but de l'interprétation abstraite est de prouver certaines propriétés sur un programme. Pour cela, nous passons par une première approximation, la sémantique collectrice, que nous approximons une seconde fois en la @@ -712,8 +702,9 @@ <subsubsection|Nouvelle notation : fonction de transition> Notons <math|\<bbb-X\>> l'ensemble des variables. On note - <math|\<bbb-X\>=\<bbb-X\><rsub|e>\<cup\>\<bbb-X\><rsub|n>> : c'est l'union - des variables de type énumération et des variables de \ type numérique. + <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 @@ -725,12 +716,12 @@ <\eqnarray*> <tformat|<table|<row|<cell|I>|<cell|=>|<cell|<around*|{|s\<in\>\<bbb-M\> - \| s<around*|(|nreset<rsub|/>|)>=t|}>>>>> + \| 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 valeurs des <em|pre>. + 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 @@ -749,14 +740,14 @@ <math|s<rsub|n>> par une fonction que l'on appellera fonction de cycle. Cette fonction copie uniquement les variables dont les valeurs précédentes sont utiles pour le calcul de la transition, et préfixe leur noms d'un - prefixe standard, ``L'', qui indique que ce sont des variables <em|last>, - c'est-à-dire qu'on a leur valeur du cycle précédent. - - La fonction de cycle <math|c : \<bbb-M\>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>> - s'occupe de faire passer les valeurs suivantes aux valeurs actuelles (nous - écrivons cette fonction comme non-déterministe car après cette fonction un - certain nombre de variables sont oubliées et on considère que leurs valeurs - n'ont pas d'importance). Elle peut être définie à partir d'un ensembles de + 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 : @@ -766,22 +757,19 @@ x|)>=s<around*|(|x|)>|}>>>>> </eqnarray*> - \; - Déroulement d'un cycle : on prend l'état <math|s> après passage par la fonction de cycle, on y met les valeurs des entrées du système. On applique ensuite la fonction <math|f : \<bbb-M\>\<rightarrow\>\<bbb-M\>> qui calcule toutes les variables du système (elle peut être définie comme la saturation - de la sémantique par réduction, comme le point fixe de l'application d'une - formule, ou plus classiquement comme l'application d'une série - d'instructions en style impératif, résultat de la compilation du + 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>>. + 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>|)>>, @@ -792,18 +780,19 @@ <subsubsection|Suppression des entrées, sémantique collectrice> - On s'intéresse maintenant à l'exécution d'un programme SCADE quel que + 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*|{|t,f|}>> qui nous dit si un environnement - est conforme à la spécification. + \<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|/>|)>=t|}>>>|<row|<cell|s<rsub|n+1><rsub|>>|<cell|=>|<cell|g<around*|(|s<rsub|n>|)>>>|<row|<cell|g<around*|(|x|)>>|<cell|=>|<cell|<big|cup><rsub|s\<in\>x><around*|{|f<around*|(|a|)>,a\<in\>c<around*|(|s|)>,q<around*|(|f<around*|(|a|)>|)>=t|}>>>>> + \| 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*> \; @@ -846,7 +835,7 @@ Cette fonction fait correspondre à une partie de <math|\<bbb-M\>> sa meilleure approximation dans le domaine abstrait (par exemple dans le cas - des polyhèdres, l'abstraction d'un ensemble fini de points est leur + 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 @@ -855,14 +844,15 @@ d'autre part. De base ici, nous avons deux choix simples pour <math|\<cal-D\><rsup|#>> : - les intervalles et les polyhèdres convexes. Ceux-ci sont considérés acquis + 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 é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>. + 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>. @@ -883,7 +873,7 @@ La fonction de transition <math|f> est représentée dans l'abstrait par une fonction <math|f<rsup|#>> qui correspond à l'application d'un certain nombre de contraintes de <math|\<bbb-E\>>, ainsi que de disjonction de cas. - On remarque que l'aspect impératif disparait complètement, on n'a plus + 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. @@ -906,6 +896,34 @@ 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 : @@ -914,7 +932,7 @@ <tformat|<table|<row|<cell|S<rsup|#>>|<cell|=>|<cell|lfp<rsub|I<rsup|#>><around*|(|\<lambda\>i.I<rsup|#>\<sqcup\>g<rsup|#><around*|(|i|)>|)>>>>> </eqnarray*> - Où <math|s<rsub|0>> est l'état initial du système et est défini par + 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>. @@ -925,9 +943,9 @@ <\itemize> <item>Contraintes numériques : les variables sont dans <math|\<bbb-X\><rsub|n>>, les constantes dans <math|\<bbb-N\>> (ou - <math|\<bbb-Q\>>), les opérateurs sont - <math|+,-,\<times\>,\<div\>,=,\<geqslant\>,\<neq\>>. On note - <math|\<bbb-E\><rsub|n>> l'ensemble de telles contraintes. + <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 @@ -945,7 +963,7 @@ </eqnarray*> Les variables booléennes peuvent être représentées par <math|0> et - <math|1>, par exemple on peut introduire les restrictions suivantes (en + <math|1>, par exemple on peut introduire les transformations suivantes (en notant <math|\<bbb-X\><rsub|b>> l'ensemble des variables à valeurs booléennes) : @@ -954,24 +972,26 @@ </eqnarray*> Les résultats sont généralement plus que médiocres. De plus, on ne peut pas - représenter ainsi les valeurs d'énumérations ayant plus de deux éléments. + 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 deux domaines + 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 selons les valeurs - des variables de <math|\<bbb-X\><rsub|e>>. Par exemple si on a un automate + 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\>>>. + fonction d'application d'une condition <math|<around*|\<llbracket\>|e|\<rrbracket\>>> + avec <math|e\<in\>\<bbb-E\><rsub|e>>. <subsection|Domaine à disjonction simple> @@ -988,97 +1008,96 @@ il faudrait noter <math|\<forall\>x\<in\>\<bbb-X\><rsub|d>>, <math|\<bbb-V\><rsub|d><around*|(|x|)>> l'ensemble des valeurs possibles pour la valeur <math|x>, qui peut être différent selon la variable - on - est ammené à faire un peu de typage, il faut en particulier s'assurer que + 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|#>> capable de gérer les contraintes sur les variables - numériques et sur les variables énumérées, mais sans relation entre les - deux. Le domaine <math|\<cal-D\><rsup|#>> représente une abstraction de - <math|\<bbb-M\><rsub|n>=<around*|(|\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>|)>\<rightarrow\>\<bbb-V\>>. - On note <math|\<bot\><rsub|n>> et <math|\<top\><rsub|n>> les éléments - bottom et top de ce treillis, <math|\<sqcup\><rsub|d>> et - <math|\<sqcap\><rsub|d>> les bornes inf et sup de ce treillis. - - La particularité des variables d'état est que l'on ne réalise pas + <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 peut le munir d'une structure de treillis : - <math|\<bbb-M\><rsub|d>\<cup\><around*|{|\<bot\>,\<top\>|}>> forme un - treillis plat : <math|\<forall\>x,y\<in\>\<bbb-M\><rsub|d>,x\<sqsubseteq\>y\<Leftrightarrow\>x=y>, - <math|\<forall\>x\<in\>\<bbb-M\><rsub|d>,\<bot\>\<sqsubset\>x\<sqsubset\>\<top\>> - (l'utilité de cette structure n'apparait pas.) On appelle toujours <math|\<bbb-M\>=\<bbb-X\>\<rightarrow\>\<bbb-V\>>, où <math|\<bbb-X\>=\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>\<cup\>\<bbb-X\><rsub|d>>. On a une injection évidente de <math|\<bbb-M\><rsub|d>> dans <math|\<cal-P\><around*|(|\<bbb-M\>|)>>, on identifie donc - <math|d\<in\>\<bbb-M\><rsub|d>> à <math|<around*|{|s\<in\>\<bbb-M\>\|\<forall\>x\<in\>\<bbb-X\><rsub|d>,s<around*|(|x|)>=\<bbb-M\><rsub|d><around*|(|x|)>|}>>. - De même on identifie <math|e\<in\>\<bbb-M\><rsub|n>> à - <math|<around*|{|s\<in\>\<bbb-M\> \| \<forall\>x\<in\>\<bbb-X\><rsub|n>\<cup\>\<bbb-X\><rsub|e>,s<around*|(|x|)>=\<bbb-M\><rsub|n><around*|(|x|)>|}>>. + <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\><rsub|d><rsup|#>>|<cell|=>|<cell|\<bbb-M\><rsub|d>\<rightarrow\>\<cal-D\><rsup|#>>>|<row|<cell|\<gamma\><rsub|d><around*|(|s|)>>|<cell|=>|<cell|<big|cup><rsub|d\<in\>\<bbb-M\><rsub|d>>d\<cap\>\<gamma\><around*|(|s<around*|(|d|)>|)>>>>> + <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\><rsub|d>>|<cell|=>|<cell|\<lambda\>d.\<bot\><rsub|n>>>|<row|<cell|\<top\><rsub|d>>|<cell|=>|<cell|\<lambda\>d.\<top\><rsub|n>>>>> + <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\><rsub|d><around*|(|\<bot\><rsub|d>|)>=\<varnothing\>> - et <math|\<gamma\><rsub|d><around*|(|\<top\><rsub|d>|)>=\<bbb-M\>>. + 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|n>t<around*|(|d|)>|)>>>|<row|<cell|s\<sqcap\>t>|<cell|=>|<cell|\<lambda\>d.<around*|(|s<around*|(|d|)>\<sqcap\><rsub|n>t<around*|(|d|)>|)>>>>> + <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\><rsub|d><rsup|#>>, + <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\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si - d<around*|(|x|)>=d<around*|(|y|)>>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>|<row|<cell|<around*|\<llbracket\>|x\<neq\>y|\<rrbracket\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si - d<around*|(|x|)>\<neq\>d<around*|(|y|)>>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>>> + <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\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si - d<around*|(|x|)>=v>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>|<row|<cell|<around*|\<llbracket\>|x\<neq\>v|\<rrbracket\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<choice|<tformat|<table|<row|<cell|s<around*|(|d|)>>|<cell|si - d<around*|(|x|)>\<neq\>v>>|<row|<cell|\<bot\><rsub|n>>|<cell|sinon>>>>>>>>> + <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. Pour toute - expression <math|e\<in\>\<bbb-E\><rsub|n>> ou - <math|e\<in\>\<bbb-E\><rsub|e>>, le domaine <math|\<cal-D\><rsup|#>> est - sensé savoir les prendre en compte de manière satisfaisante, on définit - donc : + 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\>><rsub|d><around*|(|s|)>>|<cell|=>|<cell|\<lambda\>d.<around*|\<llbracket\>|e|\<rrbracket\>><around*|(|s<around*|(|d|)>|)>>>>> + <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\><rsub|d> - t>|<cell|=>|<cell|\<lambda\>d.s<around*|(|d|)>\<nabla\>t<around*|(|d|)>>>>> + <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 @@ -1091,32 +1110,36 @@ <math|f<rsup|#>> et une fonction de cycle <math|c<rsup|#>> (par facilité, on notera <math|g<rsup|#>=c<rsup|#>\<circ\>f<rsup|#>>), l'ensemble des états accessible par le système est <math|S<rsup|#>=lfp<rsub|I<rsup|#>><around*|(|\<lambda\>s.I<rsup|#>\<sqcup\>g<rsup|#><around*|(|s|)>|)>>, - où <math|I<rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><rsub|d><around*|(|\<top\><rsub|d>|)>>. + où <math|I<rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><around*|(|\<top\>|)>>. - Définitions : pour <math|d<rsub|0>\<in\>\<bbb-M\><rsub|d>>, notons - <math|r<rsub|d<rsub|0>> : \<cal-D\><rsub|d><rsup|#>\<rightarrow\>\<cal-D\><rsub|d><rsup|#>> - tel que <math|r<rsub|d<rsub|0>><around*|(|s|)>=\<lambda\>d.<choice|<tformat|<table|<row|<cell|\<bot\>>|<cell|si + 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 : - <\eqnarray*> - <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| - s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|n>|}>>>>> - </eqnarray*> + <\itemize> + <item>Poser : - Tant que <math|\<delta\><rsub|n>\<neq\>\<varnothing\>>, on répète le - processus 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>|}>>>>> + </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|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*> + <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 connait. + 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 @@ -1126,14 +1149,16 @@ <\eqnarray*> <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| - s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|n>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>> + 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\>D<rsub|n+1><around*|(|d|)>>|<cell|si - d\<in\>K<rsub|\<nabla\>,n>>>|<row|<cell|s<rsub|n><around*|(|d|)>\<sqcup\>D<rsub|n+1><around*|(|d|)>>|<cell|sinon>>>>>>>|<row|<cell|K<rsub|\<nabla\>,n+1>>|<cell|=>|<cell|K<rsub|\<nabla\>,n>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\| - s<rsub|n><around*|(|d|)>\<neq\>\<bot\>\<wedge\>s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n>|}>>>|<row|<cell|\<delta\><rsub|n+1>>|<cell|=>|<cell|<around*|(|\<delta\><rsub|n>\\<around*|{|a<rsub|n+1>|}>|)>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\|s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n><around*|(|d|)>|}>>>>> + <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 @@ -1144,18 +1169,21 @@ permettent de réduire le domaine abstrait ? La définition précédente n'est peut-être pas la bonne, car elle risque d'appliquer des élargissements que l'on ne sait plus ensuite comment rétrécir pour refaire apparaître les - bonnes conditions. Cherchons une autre forme d'itération, par exemple : + 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|n>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>> + 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\>D<rsub|n+1><around*|(|d|)>>|<cell|si - d\<in\>K<rsub|\<nabla\>,n> et d\<neq\>a<rsub|n+1>>>|<row|<cell|s<rsub|n><around*|(|d|)>\<sqcup\>D<rsub|n+1><around*|(|d|)>>|<cell|sinon>>>>>>>|<row|<cell|K<rsub|\<nabla\>,n+1>>|<cell|=>|<cell|K<rsub|\<nabla\>,n>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\| - s<rsub|n><around*|(|d|)>\<neq\>\<bot\>\<wedge\>s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n>|}>>>|<row|<cell|\<delta\><rsub|n+1>>|<cell|=>|<cell|<around*|(|\<delta\><rsub|n>\\<around*|{|a<rsub|n+1>|}>|)>\<cup\><around*|{|d\<in\>\<bbb-M\><rsub|d>\|s<rsub|n+1><around*|(|d|)>\<neq\>s<rsub|n><around*|(|d|)>|}>>>>> + <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 @@ -1164,7 +1192,12 @@ point fixe en boucle sur lui-même. Ensuite seulement on s'occupe de savoir ce qu'il peut propager aux autres états. - <subsection|Domaine à arbre de disjonctions> + <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 @@ -1173,27 +1206,33 @@ pratique mais qui peuvent être considérés comme un traitement à part (ce n'est rien de plus que de la mémoisation et du partage). - <paragraph|Variables et contraintes.>Il y a deux domaines de variables, - <math|\<bbb-X\><rsub|e>> pour les énumérés et <math|\<bbb-X\><rsub|n>> pour - les variables numériques. Il y a deux domaines pour les contraintes, - <math|\<bbb-E\><rsub|e>> les contraintes sur les énumérés (de la forme - <math|x\<equiv\>y> ou <math|x\<equiv\>v,v\<in\>\<bbb-V\><rsub|e>>) et - <math|\<bbb-E\><rsub|n>> les contraintes sur les variables numériques - (égalités ou inégalités). + <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> - <paragraph|Domaine numérique.>On note <math|D<rsub|n>> le domaine des - valeurs numériques et <math|\<sqcup\><rsub|n>>, <math|\<sqcap\><rsub|n>>, + On note <math|D<rsub|n>> le domaine des valeurs numériques et + <math|\<sqcup\><rsub|n>>, <math|\<sqcap\><rsub|n>>, <math|<around*|\<llbracket\>|\<cdummy\>|\<rrbracket\>><rsub|n>>, <math|\<bot\><rsub|n>>, <math|\<top\><rsub|n>>, <math|\<sqsubseteq\><rsub|n>>, <math|\<matheuler\><rsub|n>>, <math|\<nabla\><rsub|n>> les éléments correspondants dans ce domaine. On considère que <math|\<gamma\><rsub|n> : - D<rsub|n>\<rightarrow\>\<cal-P\><around*|(|\<bbb-X\><rsub|e>\<cup\>\<bbb-X\><rsub|n>\<rightarrow\>\<bbb-V\>|)>> + 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>>. - <paragraph|Les EDD.>On définit un ordre sur les variables de - <math|\<bbb-X\><rsub|e>> : <math|\<bbb-X\><rsub|e>=<around*|{|x<rsub|1>,x<rsub|2>,\<ldots\>,x<rsub|n>|}>> + <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 @@ -1247,11 +1286,11 @@ L'opération <math|\<sqcap\>> est définie comme suit : <\eqnarray*> - <tformat|<table|<row|<cell|V<around*|(|t|)>\<sqcap\>V<around*|(|t<rprime|'>|)>>|<cell|=>|<cell|V<around*|(|t\<sqcap\><rsub|n>t<rprime|'>|)>>>|<row|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>\<sqcap\>C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1><rprime|'>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p><rprime|'>|)>>|<cell|=>|<cell|r<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>\<sqcap\>s<rsub|1><rprime|'>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>\<sqcap\>s<rsub|p><rprime|'>|)>>>|<row|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>\<sqcap\>s<rprime|'>>|<cell|<above|=|<text|lorsque + <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 symmétriquement lorsque <math|\<delta\><around*|(|s|)>\<gtr\>\<delta\><around*|(|s<rprime|'>|)>> + 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). @@ -1267,14 +1306,14 @@ Pour les conditions sur les énumérés, on définit d'abord : <\eqnarray*> - <tformat|<table|<row|<cell|c<around*|(|x\<equiv\>v|)>>|<cell|=>|<cell|C<around*|(|x,v\<rightarrow\>V<around*|(|\<top\>|)>,v<rprime|'>\<rightarrow\>V<around*|(|\<bot\>|)>,v<rprime|'>\<in\>\<bbb-V\><rsub|e>\\<around*|{|v|}>|)>>>|<row|<cell|c<around*|(|x\<nequiv\>v|)>>|<cell|=>|<cell|C<around*|(|x,v\<rightarrow\>V<around*|(|\<bot\>|)>,v<rprime|'>\<rightarrow\>V<around*|(|\<top\>|)>,v<rprime|'>\<in\>\<bbb-V\><rsub|e>\\<around*|{|v|}>|)>>>|<row|<cell|c<around*|(|x<rsub|i>\<equiv\>x<rsub|j>|)>>|<cell|<above|=|lorsque + <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 symmétriquement lorsque <math|j\<gtr\>i>. + et symétriquement lorsque <math|j\<gtr\>i>. - On peut ensuite poser : + 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>>>> @@ -1291,8 +1330,10 @@ i\<less\>\<delta\><around*|(|s<rprime|'>|)>>>|<cell|<big|wedge><rsub|i=1><rsup|p>s<rsub|i>\<sqsubseteq\>s<rprime|'>>>>> </eqnarray*> - <paragraph|Opérateur de widening.>Sur nos EDD, on définit une opération - <math|\<rho\>:D<rsub|n>\<times\>D\<rightarrow\>D> comme suit : + <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 @@ -1306,7 +1347,7 @@ <\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 + \<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*> @@ -1315,30 +1356,33 @@ <math|\<sqcup\>>, plus on passe <math|a> et <math|b> à notre fonction <math|f<rsub|\<nabla\>>>). Explication : lorsque l'on doit faire l'union de deux feuilles, on fait un widening si et seulement si les deux feuilles - sont accessibles selont exactement la même formule booléenne sur les + sont accessibles selon exactement la même formule booléenne sur les énumérés dans <math|a> et <math|b>. - <paragraph|Itérations chaotiques.>On enrichit un peu notre arbre au niveau - des feuilles pour enregistrer quelques informations supplémentaires : + <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 à : ``cette feuille est nouvelle, il faut l'analyse - comme nouveau cas'', et l'indice <math|i\<in\>\<bbb-N\>> correspond à : - ``cette feuille est là depuis <math|n> itérations'', où le <math|n> permet + 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 définit maintenant une fonction d'accumulation <math|\<diamond\>> comme - suit (<math|\<tau\>> correspond à un delai 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,V<around*|(|\<bot\><rsub|n>|)><rsub|>,V<around*|(|t|)>|)>>|<cell|<above|=|lorsque - t\<neq\>\<bot\><rsub|n>>>|<cell|V<around*|(|t|)><rsub|0>>>|<row|<cell|f<rsub|\<diamond\>><around*|(|a,b,V<around*|(|t|)><rsub|i><rsup|\<nu\>>,V<around*|(|\<bot\><rsub|n>|)>|)>>|<cell|=>|<cell|V<around*|(|t|)><rsub|i><rsup|\<nu\>>>>|<row|<cell|f<rsub|\<diamond\>><around*|(|a,b,V<around*|(|t|)><rsub|i><rsup|\<nu\>>,V<around*|(|t<rprime|'>|)>|)>>|<cell|=>|<cell|<choice|<tformat|<table|<row|<cell|V<around*|(|t - \<nabla\><rsub|n>t<rprime|'>|)><rsub|i+1><rsup|\<nu\>>>|<cell|si - \<rho\><around*|(|t,a|)>=\<rho\><around*|(|t<rprime|'>,b|)>\<wedge\> + 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*> @@ -1356,7 +1400,8 @@ <around*|(|\<rho\><around*|(|t,s|)>\<sqcap\>s|)>\<nsqsubseteq\>s<rsub|0>>>|<row|<cell|V<around*|(|t|)><rsub|i>>|<cell|sinon>>>>>>>|<row|<cell|f<rsub|\<oast\>><around*|(|s<rsub|0>,s,V<around*|(|t|)><rsub|i><rsup|\<ast\>>|)>>|<cell|=>|<cell|V<around*|(|t|)><rsub|i><rsup|\<ast\>>>>|<row|<cell|f<rsub|\<oast\>><around*|(|s<rsub|0>,s,C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>s<rsub|1>,\<ldots\>,v<rsub|p>\<rightarrow\>s<rsub|p>|)>|)>>|<cell|=>|<cell|C<around*|(|x<rsub|i>,v<rsub|1>\<rightarrow\>f<rsub|\<oast\>><around*|(|s<rsub|0>,s,s<rsub|1>|)><rsub|>,\<ldots\>,v<rsub|p>\<rightarrow\>f<rsub|\<oast\>><around*|(|s<rsub|0>,s,s<rsub|p>|)>|)>>>>> </eqnarray*> - On commence avec : + 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\>> @@ -1384,7 +1429,7 @@ de widening convenable) Dans tous les cas, on refait une itération. Les étoiles finiront bien par - disparaitre. + disparaître. <item>Si il n'existe pas de telle feuille étoilée dans <math|s<rsub|n>> : @@ -1395,6 +1440,10 @@ Dans ce cas, on s'arrête si <math|s<rsub|n+1>=s<rsub|n>>. </itemize> + + <section|Implémentation> + + \; </body> <\initial> @@ -1422,12 +1471,15 @@ <associate|auto-22|<tuple|5|11>> <associate|auto-23|<tuple|5.1|11>> <associate|auto-24|<tuple|5.2|13>> - <associate|auto-25|<tuple|5.2.0.1|13>> - <associate|auto-26|<tuple|5.2.0.2|13>> - <associate|auto-27|<tuple|5.2.0.3|13>> - <associate|auto-28|<tuple|5.2.0.4|15>> - <associate|auto-29|<tuple|5.2.0.5|15>> + <associate|auto-25|<tuple|5.2.1|13>> + <associate|auto-26|<tuple|5.2.2|13>> + <associate|auto-27|<tuple|5.2.3|13>> + <associate|auto-28|<tuple|5.2.4|15>> + <associate|auto-29|<tuple|5.2.5|15>> <associate|auto-3|<tuple|2.1|1>> + <associate|auto-30|<tuple|5.2.3.3|?>> + <associate|auto-31|<tuple|5.2.5.2|?>> + <associate|auto-32|<tuple|6|?>> <associate|auto-4|<tuple|2.2|2>> <associate|auto-5|<tuple|2.3|2>> <associate|auto-6|<tuple|2.3.1|3>> @@ -1477,7 +1529,7 @@ <no-break><pageref|auto-9>> <with|par-left|<quote|3fn>|2.3.5<space|2spc>Règles de réduction pour - les affectations <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + 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 |