Raffinement de Programmes [SuitableStuff]

- Raffinement de Programmes
  - Simplification par la relation de raffinement
  - Raffinement assurant la terminaison
- Raffinement de spécifications

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`

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 < V₀) 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. V₀ est la valeur de V dans l'état initial. On peut omettre cette condition si on veut se contenter de correction partielles.