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⟧}[_]$

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$    

Leave a comment