###### tags: `TAS`
@mamy @theOnlyAlex @wlin @nlejeune @gnouf

# TAS - TD 8

[e-mail]

$$E = v \to P(\mathbb{Z})$$

1. $$
\mathbb{E}[[rand(a, b)]]: E \to P(\mathbb{Z}) \\
\mathbb{E}[[rand(a, b)]] \rho = \{ x | a \leq x \leq b\}
$$

2. $$
\mathbb{E}[[rand(0, 2) + 3 \times v]] \rho = \{ v_1 + v_2\ |\ v_1 \in \mathbb{E} [[rand(0, 2)]] \rho, v2 \in \mathbb{E} [[3 \times v]] \} \\
v_1 \in [0, 1, 2]\ \ \ ,\ \ v_2 \in [v_3 . v_4\ |\ v_3 \in \mathbb{E} [[3]]] \rho\ \ ,\ \ v_4 \in \mathbb{E} [[v]] \rho \\
= \{v_1 + v_2\ |\ v1 \in [0, 1, 2], v_2 = 3 \rho (v)\} \\
= \{3 \rho (v) ; 3 \rho (v) + 1; 3 \rho (v) + 2\}
$$

3. $$
0 \to \{v \to 0\} \\
1 \to
\Bigg\{
\begin{pmatrix}
v \to 0 \\
u \to 0
\end{pmatrix}
\Bigg\} \\
2 \to
\Bigg\{
\begin{pmatrix}
v \to 0 \\
a \to 0
\end{pmatrix}
\begin{pmatrix}
v \to 1 \\
a \to 0
\end{pmatrix}
\Bigg\} \\
3 \to
\Bigg\{
\begin{pmatrix}
0 \\ 0
\end{pmatrix},
\begin{pmatrix}
0 \\ 1
\end{pmatrix},
\begin{pmatrix}
0 \\ 2
\end{pmatrix},
\begin{pmatrix}
1 \\ 3
\end{pmatrix},
\begin{pmatrix}
1 \\ 4
\end{pmatrix},
\begin{pmatrix}
1 \\ 5
\end{pmatrix}
\Bigg\} \\
4 \to
\Bigg\{
\begin{pmatrix}
0 \\ 0
\end{pmatrix},
\begin{pmatrix}
0 \\ 1
\end{pmatrix},
\begin{pmatrix}
0 \\ 2
\end{pmatrix}
\Bigg\}
$$

4. $$
filter: t \to bool\_expr\ ent \to bool \to t \\
\mathbb{e} [[bexpr]] \\
\mathbb{c}[[bexpr]](R) = filter\ R\ bexpr\ true \\
\mathbb{C} [[\neg\ bexpr]](R) = filter\ R\ bexpr\ false \\
(a \leq 2)\ false
$$

5. $\ \ \ \mathbb{S} [[$``x = 2 * rand(0, 1); if(x == 0) { x = x+1; } else { x = x-1; }`` $]]\mathbb{R}$
= $\mathbb{S} [[$ ``if (x == 0) { x = x+1; } else { x = x-1; }`` $]] \big(\mathbb{S} [[$ ``x = 2 * rand(0, 1)`` $]] \mathbb{R} \big)$
= $\mathbb{S} [[$ ``x = x+1;`` $]] $\big( \mathbb{C} [[ ``x == 0`` ]] \mathbb{R}'\ \cup\ \mathbb{S} [[$ (à terminer)