TD6 : Sémantique

Simon Halfon :

halfon@lsv.fr

EX 1

ABS :

Supposons que $∃ 𝜌’; 𝜌 \vdash$ while 1 do skip $⟹ 𝜌’$

est dérivable, alors soit $𝜋$ une dérivation minimale.

Donc par analyse de cas, elle termine par la règle “while” :

⋯	⋯
$𝜋_1$	$𝜋_2$
$𝜌\vdash skip ⟹ 𝜌’’$	$𝜌\vdash $ while 1 do skip $⟹ 𝜌’$
$𝜌\vdash $ while 1 do skip $⟹ 𝜌’$

Or :

$𝜌\vdash skip ⟹ 𝜌’’$ implique que

\[𝜌=𝜌''\]

donc $𝜋$ n’est pas minimal : absurde.

EX 2

1.

$c_1 ≝ $ while e do c

$\overset{?}{\sim}$

$c_2 ≝ $ if e then (c; while e do c) else skip

Soit $𝜌, 𝜌’$ des environnements.

⟹ : Si $𝜌 \vdash$ while e do c $⟹ 𝜌’$

Montrons que :

$𝜌 \vdash $ if e then (c; while e do c) else skip $ ⟹ 𝜌’$

• Cas 1 : si $⟦e⟧𝜌 ≠0$ :

Alors on a l’arbre de preuve suivant (while):

⋯	⋯
$𝜋_1$	$𝜋_2$
$𝜌\vdash c ⟹ 𝜌’’$	$𝜌’‘\vdash $ while e do c $⟹ 𝜌’$
	$𝜌\vdash $ while e do c $⟹ 𝜌’$

on veut avoir :

⋯
$𝜌\vdash $ (c; while e do c) $⟹ 𝜌’$
$𝜌\vdash $ if e then (c; while e do c) else skip $⟹ 𝜌’$

Or, avec (Seq) :

⋯	⋯
$𝜌\vdash c ⟹ 𝜌’’$	$𝜌’‘\vdash $ while e do c $⟹ 𝜌’$
	$𝜌\vdash $ (c; while e do c) $⟹ 𝜌’$

Donc

⋯	⋯
$𝜌\vdash c ⟹ 𝜌’’$	$𝜌’‘\vdash $ while e do c $⟹ 𝜌’$
	$𝜌\vdash $ (c; while e do c) $⟹ 𝜌’$
	$𝜌\vdash $ if e then (c; while e do c) else skip $⟹ 𝜌’$

• Cas 2 : si $⟦e⟧𝜌 =0$ :

Alors on a l’arbre de preuve suivant (while_fin):

$𝜌\vdash $ while e do c $⟹ 𝜌’$

on veut avoir (if_2) :

⋯
$𝜌\vdash $ skip $⟹ 𝜌’$
$𝜌\vdash $ if e then (c; while e do c) else skip $⟹ 𝜌’$

ce qui force $𝜌 = 𝜌’$

Or, avec (Skip) :

$𝜌\vdash skip ⟹ 𝜌$

Donc on peut conclure.

2.

Ce sont les programmes qui ne terminent jamais.

3.

1.

Par récurrence sur le max $h$ des hauteurs des deux arbres de preuve de $𝜌\vdash c ⟹ 𝜌_1$ et $𝜌\vdash c ⟹ 𝜌_2$

• Initialisation : si $h=1$ : on dans un des cas de base :

  • Cas des base : $skip$, :=, ou $while_{fin}$

• Hérédité :

  • On ne fait que le while, par exemple :
    • il suffit de remarquer que, comme $c$ est le même dans les deux arbres, les avant-dernières formules sont contraintes
    • puis : on applique l’hypothèse d’induction à $𝜌’_1$, $𝜌’_2$ pour obtenir $𝜌’_1 = 𝜌’_2$
    • puis : de même, hypothèse d’induction à $𝜌_1$ et $𝜌_2$ pour en déduire l’égalité.

2.

On ajoute deux règles :

$𝜌\vdash c_1 ⟹ 𝜌’$
$𝜌\vdash c_1 ∨ c_2 ⟹ 𝜌$

et

$𝜌\vdash c_2 ⟹ 𝜌’$
$𝜌\vdash c_1 ∨ c_2 ⟹ 𝜌$