TD9 : Sémantique

EX 1

1.

M1 :

Si $A⟶B$ et $A⟶B’$.

En reprenant l’exemple du groupe libre du cours d’algèbre, on peut montrer que $B = f(A) = B’$ où est obtenue par propriété universelle de manière unique.

M2 :

Les deux règles ne peuvent pas s’appliquer à un $A$ donné.

2.

Montrons que \(A⟶^\ast B ⟹ ⟦A⟧=⟦B⟧\)

il suffira de montrer que

\[A⟶B ⟹ ⟦A⟧=⟦B⟧\]

c’est clair car

\[⟦A⟧ = \vert A \vert \mod 2\]

Or, si $A⟶B$, $\vert A \vert = \vert B \vert +2$.

3.

vient du fait que :

\[⟦A⟧ = \vert A \vert_\ast - \vert A \vert_\bullet\]

4.

Abstraction complète :

\[⟦A⟧=⟦B⟧ ⟺ A≃B\]

i.e

\[⟦A⟧=⟦B⟧ ⟺ ∀C, (C[A] ⟶^\ast 𝜀 ⇔ C[B] ⟶^\ast 𝜀)\]

NB :

\[C = \ast \bullet \ast [\_] \ast \ast \\ C[A] = \ast \bullet \ast A \ast \ast\]

Pour la sémantique 1 :

\[⟦A⟧=⟦B⟧ \not⟹ (C[A] ⟶^\ast 𝜀 ⇔ C[B] ⟶^\ast 𝜀)\]

Contre-ex :

• $C = 𝜀[]$
• $A = \ast \bullet$
• $B = \ast \ast$

alors

\[⟦A⟧ = 0 = ⟦B⟧\]

mais

$C[A]⟶𝜀$ et $C[B]\not⟶𝜀$

---

Pour la sémantique 2 :

• ⟹ : Si $\vert A \vert_\ast - \vert A \vert_\bullet = ⟦A⟧ = ⟦B⟧ = \vert B \vert_\ast - \vert B \vert_\bullet$, alors :

On remarque que

\[\begin{align*} C[A] ⟶^\ast 𝜀 &⟺ \vert C[A] \vert_\ast = \vert C[A] \vert_\bullet \\ &⟺ \vert C[𝜀] \vert_\ast + \vert A \vert_\ast = \vert C[𝜀] \vert_\bullet + \vert A \vert_\bullet \\ &⟺ \vert C[𝜀] \vert_\ast + \vert A \vert_\bullet + \vert B \vert_\ast - \vert B \vert_\bullet = \vert C[𝜀] \vert_\bullet + \vert A \vert_\bullet \\ &⟺ \vert C[𝜀] \vert_\ast + \vert B \vert_\ast = \vert C[𝜀] \vert_\bullet + \vert B \vert_\bullet \\ &⟺ C[B] ⟶^\ast 𝜀 \end{align*}\]

NB : On peut remarquer que :

\[X ⟶^\ast \begin{cases} \ast^{⟦X⟧} \text{ si } ⟦X⟧≥0 \\ \bullet^{-⟦X⟧} \text{ si } ⟦X⟧<0 \end{cases}\]

• ⟸ : si $(C[A] ⟶^\ast 𝜀 ⇔ C[B] ⟶^\ast 𝜀)$

alors :

\[\vert C[𝜀] \vert_\ast + \vert A \vert_\ast = \vert C[𝜀] \vert_\bullet + \vert A \vert_\bullet ⟺ \vert C[A] \vert_\ast = \vert C[A] \vert_\bullet \\ ⟺ C[A] ⟶^\ast 𝜀 ⟺ C[B] ⟶^\ast 𝜀 ⟺ \vert C[B] \vert_\ast = \vert C[B] \vert_\bullet \\ ⟺ \vert C[𝜀] \vert_\ast + \vert B \vert_\ast = \vert C[𝜀] \vert_\bullet + \vert B \vert_\bullet\]

---

Si $A≃B$ $∀C$,

si $∀C, (C[A] ⟶^\ast 𝜀 ⇔ C[B] ⟶^\ast 𝜀)$

$C[_] = a^{-⟦A⟧}[_]$

où

\[a^x = \begin{cases}\ast^{x} \text{ si } x≥0 \\ \bullet^{-x} \text{ si } x<0 \end{cases}\]

$C[A]⟶^\ast 𝜀, C[B]⟶^\ast 𝜀$

$a^{-⟦A⟧}B⟶^\ast 𝜀$

$-⟦A⟧ + ⟦B⟧ = ⟦a^{-⟦A⟧}⟧ + ⟦B⟧ = ⟦a^{-⟦A⟧}B⟧=0$

EX 2

1.

Montrons que tout triplet de Hoare prouvable est valide.

Dém :

Par induction structurelle sur l’arbre de preuve.

• Initialisation : immédiate pour skip.

Pour l’affectation $x:=e$ :

soit $𝜌$ un environnement tel que

\[𝜌\vDash 𝜑∧⟦c⟧𝜌 ≠ \bot\]

où $⟦c⟧𝜌 = 𝜌[x:=e]$

alors on a bien :

\[𝜌[x ← e] \vDash 𝜑\]

• Hérédité :

Soit $𝜌$ un environnement tel que

\[𝜌\vDash 𝜑∧⟦c⟧𝜌 ≠ \bot\]

Si

$\lbrace 𝜑∧b\rbrace c_1 \lbrace 𝜓 \rbrace$	$\lbrace 𝜑∧ \lnot b\rbrace c_2 \lbrace 𝜓 \rbrace$
$\lbrace 𝜑 \rbrace \textsf{ if } b \textsf{ then } c_1 \textsf{ else } c_2 \textsf{ fi } \lbrace 𝜓 \rbrace$

Si $𝜌\vDash b$, alors $𝜌\vDash 𝜑$ implique que $𝜌\vDash 𝜑∧b$

Donc par hypothèse d’induction, $⟦c_1⟧𝜌 \vDash 𝜓$

Si $𝜌\vDash b$, alors $⟦c_1⟧𝜌 = ⟦c⟧𝜌 \vDash 𝜓$

Si $𝜌\vDash \lnot b$ : analogue.

---

On procède de même pour les autres triplets de Hoare.

2.

Correction partielle :

$\lbrace 𝜑 ∧ e \rbrace c \lbrace 𝜑 \rbrace$
$\lbrace 𝜑 \rbrace \textsf{ while } e \textsf{ do } c \lbrace 𝜑 ∧ \lnot e\rbrace$

$\lbrace 𝜑 \rbrace c_1 \lbrace 𝜑’\rbrace$	$\lbrace 𝜑’ \rbrace c_2 \lbrace 𝜓\rbrace$
$\lbrace 𝜑 \rbrace c_1; c_2 \lbrace 𝜓\rbrace$

3.

$\lbrace x=0 ∧ y=0 ∧ z=0 ∧ n≥0\rbrace \textsf{ while } z < 3n \textsf{ do } z := z+3; y:=y+2z-3; x:=x+y-z+1 \lbrace x=n^3\rbrace$

$I = 27x^3= z^3 ∧ 9y = z^2 + 67 ∧ z≤3n$

$\lbrace 𝜑 ∧ b \rbrace c \lbrace 𝜑 \rbrace$
$\vDash 𝜑 ⟹ I$	$\lbrace I\rbrace c \lbrace I∧z≥3n\rbrace$	$\lbrace I∧z≥3n\rbrace ⟹ x=n^3$
$\lbrace \underbrace{x=0 ∧ y=0 ∧ z=0 ∧ n≥0}{≝ 𝜑}\rbrace \textsf{ while } z < 3n \textsf{ do } z := z+3; y:=y+2z-3; x:=x+y-z+1 \lbrace \underbrace{x=n^3}{≝𝜓}\rbrace$