Raffinement de Programmes

Le raffinement établit une relation entre des programmes.

raffine

on dit qu'un programme P' raffine un programme P, ou bien que P est raffiné par P', et on note P \sqsubseteq P', si et seulement si P' satisfait toute spécification que P satisfait. C'est à dire, P \sqsubseteq P'\; \Leftrightarrow P sat S ⇒ P' sat S, où sat est la propriété de satisfaction choisie.

La propriété de satisfaction peut être par exemple

  • la correction partielle.
    • P \sqsubseteq P' \Leftrightarrow \forall p,q\quad \left\{p\right\}P\left\{q\right\} \Rightarrow \left\{p\right\}P'\left\{q\right\}
  • la correction total :
    • P \sqsubseteq P'\quad \Leftrightarrow \forall post, wp\left(P,post\right)\Rightarrow \; wp\left(P',post\right). En particulier, wp\left(P,vrai\right)\Rightarrow \; wp\left(P',vrai\right) : si P termine, alors P' termine aussi.

Exemples de programmes non-comparables par la relation de raffinement :

a)

P = if n ≥ 0 then n:=0 else n:=1
P' : n:=0
  • wp(P, n=0) = (n ≥ 0) ⇒ wp(P', n=0) = vrai
  • wp(P, n=1) = (n < 0) ⇐ wp(P', n=1) = faux : donc on n'a pas P \sqsubseteq P' ni le contraire.

b)

P = n:=n; while (i>0) do {i:=i-1}
P' = i:=0
  • wp(P, i=0) = (n ≥ 0) ⇒ wp(P, i=0) = vrai
  • wp(P, i<0) = (n < 0) ⇐ wp(P', i<0) = faux : donc on n'a pas P \sqsubseteq P' ni le contraire.

Simplification par la relation de raffinement

Voici un exemple de simplification par la relation de raffinement :

P P'
i:=n*n
while i>0 do
i:=i-1
i:=0

On a bien P \sqsubseteq P' (et aussi P' \sqsubseteq P ). Les deux programmes se raffinement mutuellement : ils sont équivalents.

Raffinement assurant la terminaison

Voici un exemple d'un programme P qui peut ne pas terminer, et son raffinement P' qui termine toujours.

P P'
while (i <> n) do
i:=i+1
while (i < n) do \\i:=i+1

Raffinement de spécifications

On peut étendre le raffinement aux spécifications, pour être défini, qu'il s'agisse de programmes, de spécifications ou d'énoncés mixtes mêlant des morceaux de programmes et de spécifications en cours de transformation. Pour cela, la notion de weakest precondition est étendue aux spécifications :

  • wp([p,q], post) = p ∧ (q ⇒ post)

Propriétés

  • affaiblissement de la pré-condition : si p ⇒ p' alors \left[p,q\right] \sqsubseteq \left[p', q\right]
  • renforcement de la post-condition : si q' ⇒ q alors \left[p,q\right] \sqsubseteq \left[p, q'\right]

Exemples

\left[vrai, x\geq0\right] \sqsubseteq \left[vrai, x=0\right], ce qui signifie qu'un programme qui met x à 0 satisfait la spécification qui impose que x soit non-négatif.

\left[0 \leq x \leq 9, y^2 = x\right]
\sqsubseteq \left[0 \leq x \leq 9, y^2 = x \;\wedge\;y\geq 0\right]
\sqsubseteq \left[0 \leq x , y^2 = x \;\wedge\;y\geq 0\right]
\sqsubseteq \left[\text{vrai}, y^2 = x \;\wedge\;y\geq 0\right]

Cette dernière spécification est non-implémentable, on peut aller trop loin.

Dérivation d'un programme à partir d'une spécification

Le raffinement est un processus continu : on obtient une spécification raffinée en raffinant un morceau de cette spécification. On introduit progressivement une notation de programme à partir d'une spécification.

Par exemple, ça peut s'opérer par la composition séquentielle de spécifications :

  • \forall p, q , r : \left[p,q\right] \sqsubseteq \left[p,r\right];\left[r,q\right]

Pour dériver un programme complètement, il suffit de re-appliquer cette technique jusqu'à des briques de base pour lesquelles le passage spécification-programme est prédéfini. On peut ainsi définir des règles de raffinement élémentaires qui permettent de passer d'une spécification implémentable à un programme impératif.

Règles de raffinement de de Morgan

par une affectation si pre ⇒ post [x\exp] alors \left[pre,post\right] \sqsubseteq x:=\text{exp}
par une instruction vide si p→q alor \left[p,q\right] \sqsubseteq \text{ skip}
par un séquence \left[p,q\right] \sqsubseteq \left[p,r\right];\left[r,q\right]
par une alternative \left[p,q\right]\;\sqsubseteq\;\text{ if }b\text{ then } \left[p\wedge b,q\right]\text{ else }\left[p \wedge \neg b, q\right]
par une itération \left[I, I\wedge \neg b\right] \text{ while }b\text{ do } \left[I\wedge b, I\wedge 0\leq V \lt V_0 \right]
La condition (0 ≤ V < V0) est ajoutée pour garantir la terminaison, où V est une expression (variant) choisie de façon à ce que ses valeurs entières décroissent strictement à chaque étape de l'itération et n'atteignent jamais la valeur 0. V0 est la valeur de V dans l'état initial. On peut omettre cette condition si on veut se contenter de correction partielles.

E.g. Maximum de 2 nombres

E.g. échange de 2 variables

E.g. puissance de 2

E.g. factorielle


 
m1ilc/semantics_9.txt · Dernière modification: 2010/05/26 18:51 par suitable