###### tags: `TAS` @mamy @theOnlyAlex @wlin @nlejeune @gnouf # TAS - TD 9 ## Exercice 1 1. $$ \mathbb{S}(\gamma[[stnt]](S^\#)) \subseteq \gamma (\mathbb{S}[[stnt]](S^\#)),\ \forall\ S^\#,\ \forall\ stnt. $$ 2. $$ S^\# \sqsubseteq \mathbb{C}[[bexpr]] S^\# \\ \mathcal{D}^\# = \mathcal{P}(\mathcal{E}) \\ \mathbb{C}^\#[[bexpr]] S^\# = S^\# \\ \gamma : \mathcal{D}^\# \to \mathcal{P(E)} $$ ##### a. Montrer que $\mathbb{C}$ est sûre $$ \gamma (\mathbb{C}^\# [[bexpr]] S^\#) = \gamma(S^\#) = S^\# \\ \mathbb{C}[[bexpr]](\gamma (S^\#)) \subseteq \gamma (S^\#) $$ ##### b. Trouver $S^\#,\ bexpr$ tels que $S^\# \sqsubseteq \mathbb{C}^\# [[bexpr]] S^\#$, mais tels que $S^\#$ ne satisfasse pas $bexpr$. $$ S^\# = \{ (x \mapsto 0), (x \mapsto 1) \} \\ bexpr = x == 1 \\ $$ ​ $\Rightarrow$ certains environnements $(x \to 0)$ sont gardés alors qu'ils ne respectent pas $bexpr$. 3. $$ filter\ S^\#\ bexpr\ false \sqsubseteq\ \perp \\ \Rightarrow \mathbb{C}^\# [[\neg bexpr]] S^\# \sqsubseteq\ \perp \\ \Rightarrow \gamma(\mathbb{C}^\# [[\neg bexpr]] S^\#) = \emptyset \\ \Rightarrow \mathbb{C}[[\neg bexpr]](\gamma (S^\#)) \subseteq \gamma (\mathbb{C}^\# [[\neg bexpr]] S^\#) = \emptyset \\ \Rightarrow \mathbb{C} [[\neg bexpr]] \gamma (S^\#) = \emptyset $$ ​ Donc tous les environnements de $V(S^\#)$ satisfont bien $bexpr$. ## Exercice 2 1. Non (comment contourner le problème ? $\to$ cf cours 1). 2. $$ \mathbb{S} [[boucle]] R = \mathbb{C} [[\neg rand(0, 1) == 0]] (lfp\ F) \\ F(X) = R\ \cup\ \mathbb{S}[[if\ (i < 2)\ \{\ i = i+1;\ \}]] (\mathbb{C} [[rand(0, 1) == 0]]X) \\ \\ \mathbb{C} [[rand(0, 1) == 0]] S = S \\ \mathbb{S} [[if(i < 2)\ \{\ i = i+1;\ \}]] S = \mathbb{S} [[i = i+1]] (\mathbb{C} [[i < 2]] S) \\ R = \{(i \mapsto 0)\} $$ Après simplifications : $\mathbb{S} [[boucle]] R = lfp\ F$ avec $F(X) = \{ (i \mapsto 0) \} \cup \mathbb{S} [[i = i+1]] (\mathbb{C} [[i < 2]] X)$ 3. Via le théorème de Kleene(x) ![](https://i.imgur.com/oxaC5dY.png =50x50) $lfp\ F = \underset{n \in \mathbb{N}}{\cup} F^n (\emptyset)$ $$ F^0(\emptyset) = \emptyset \\ \\ F^1(\emptyset) = \{ (i \mapsto 0) \} \cup \mathbb{S} [[i = i+1]] (\mathbb{C}[[i < 2]] \emptyset) = \{ (i \mapsto 0) \} \\ \\ F^2(\emptyset) = F(F(\emptyset)) = F(\{ (i \mapsto 0) \}) = \{ (i \mapsto 0) \} \cup \mathbb{S} [[i = i+1]] (\mathbb{C} [[i < 2]] \{ (i \mapsto 0) \}) = \{ (i \mapsto 0), (i \mapsto 1) \} \\ \\ F^3(\emptyset) = F(F^2(\emptyset)) = \{ (i \mapsto 0) \} \cup \mathbb{S} [[i = i+1]] (\mathbb{C} [[i < 2]] \{ (i \mapsto 0) \}) \{ (i \mapsto 0), (i \mapsto 1) \} = \{ (i \mapsto 0), (i \mapsto 1), (i \mapsto 2) \} \\ \\ F^4(\emptyset) = F(F^3(\emptyset)) = \{ (i \mapsto 0) \} \cup \mathbb{S} [[i = i+1]] (\mathbb{C} [[i < 2]] \{ (i \mapsto 0) \}) \{ (i \mapsto 0), (i \mapsto 1), (i \mapsto 2) \} \\ = \{ (i \mapsto 0) \} \cup \mathbb{S} [[i = i+1]] \{ (i \mapsto 0) \}) \{ (i \mapsto 0), (i \mapsto 1) \} = F^3(\emptyset) $$ ​ $\Rightarrow lfp\ F = F^3(\emptyset)$