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

Leave a Comment