TD12 : flux d’information sûrs

TD : flux d’information sûrs

1.

Le résultat est n’est non trivial que pour les règles $({\sf let})$ et ${\sf while_1}$ : les autres règle ne modifiant ni l’image de $𝜌$, ni le domaine de $𝜇$.

• Pour ${\sf let}$ :

  il suffit de montrer que $Im(𝜌) ⊆ Dom(𝜇’\backslash \lbrace l \rbrace)$

  Or :

  \[l = alloc(Dom(𝜇))∉Dom(𝜇)\]

  Donc comme $Im(𝜌)⊆Dom(𝜇)$ par hypothèse d’induction, le résultat est acquis.

• Pour ${\sf while_1}$ :

  c’est clair par hypothèse d’induction

2.

1.

D’après la règle $Let$, le type $𝜏’$ de l’expression $y$ est égal au type de $x$.

Or, on peut toujours surprotéger une variable : i.e toute variable d’un type faible est aussi une expression d’un type plus fort (par la règle $Expr$).

Donc

\[𝜏≤𝜏'\]

2.

Si $𝛤 \vdash x := e : 𝜏$ est dérivable