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

# TAS - TD 11

## Exercice 1

{
    int i;
    int v;
    v = rand(0, 3);
    while(i < 4) {
        i = i + 1;
        v = 3 * v + 1;
        if(v > 64) { v = 63; }
        print_all;
    }
    print_all;
}

1. $$
F^n(\bot) \\
F^\#(X^\#) = R^\# \sqcup^\# \mathbb{S}[[body]].\mathbb{C}^\#[[cond]]X^\# \\
R^\#: Etat\ avant\ boucle
$$

| n | **$F^{\#, n}(\bot)$** |
| :--: | :-----------: |
| 0 | $\bot$ |
| 1 | $R^\# = \{ i \mapsto [0, 0], v \mapsto [0, 3] \}$ |
| 2 | $F^{\#, 2}(\bot) = F^\#(R^\#)=R^\# \sqcup^\# \underbrace{\mathbb{S}^\#[[body]]R^\#}_{\Bigg\{ \begin{matrix} i \mapsto [1, 1] \\ v \mapsto [1, 10] \end{matrix}} = \Bigg\{ \begin{matrix} i \mapsto [0, 1] \\ v \mapsto [0, 10] \end{matrix}$<br />$R^\# = \{ i \mapsto [0, 1], v \mapsto [0, 10] \}$ |
| 3 | $R^\# = \{ i \mapsto [0, 2], v \mapsto [0, 31] \}$ |
| 4 | $\mathbb{S}^\# [[if\ (v > 64)\{ v = 63 \}]] \Bigg\{ \begin{matrix} i \mapsto [1, 3] \\ v \mapsto [63, 63] \sqcup^\# [0, 64] = [0, 64] \end{matrix}$<br />$R^\# = \{ i \mapsto [0, 3], v \mapsto [0, 64] \}$ |
| 5 | $R^\# = \{ i \mapsto [0, 4], v \mapsto [0, 64] \}$ |
| | $[0, 4], [0, 64]$ |