IV. Raffinement de Programmes

L'aspect preuve de programmes a un dual naturel qui est la réalisation d'un programme à partir d'une spécification. Par exemple, en se basant sur la logique de Hoare pour les programmes impératifs :

• preuve : étant donné un programme P, prouver que ce programme admet deux prédicats p et q comme pré- et post- conditions.
• dérivation : étant donné deux prédicats p et q, prouver un programme P qui admette ces deux prédicats comme pré- et post- conditions (on utilise les règles de la logique de Hoare dans l'autre sens).

On s'est référé précédemment à une forme de spécification dite pré-post. Nous étudierons ces spécifications dans la suite. De manière plus générale, on peut dire qu'un programme définit une relation des données et des résultats. Une première idée lorsqu'on parle de spécification est donc d'exprimer une relation en logique de 1^ère ordre.

Les modes de programmation logique et fonctionnel sont sans variables au sens informatique, donc sans effet de bord, alors que c'est ce qui caractérise la programmation impérative. La programmation impérative est un mode de programmation par effets (avec des variables au sens informatique). Cette différence fondamentale pose le problème de la dérivation d'un programme satisfaisant un spécification donnée.

Une solution consiste à définir une spécification comme une paire [p, q] de prédicats caractérisant les états mémoire d'une machine abstraite.

Cette notion va permattre de défiir formellement la raffinement de programmes ou de spécifications. C'est aussi un cadre approprié pour définir une sémantique dite axiomatique du langage considéré.

weakest precondition

soient P un énoncé et post un prédicat. On appelle weakest precondition du couple (P,post) et on note wp(P,post) le plus faible prédicat suffisant pour qu'à partir de l'état mémoire qu'il décrit l'exécution de P termine dans un état mémoire qui satisfait post.

Un énoncé P apparait comme un ransformateur de prédicat que à post associe wp(P,post). Ceci définit la sémantique axiomatique de l'énoncé P.

transformateur

pour le langage L, les opérations de transformation sont les suivantes :

• wp(x:=exp, post) = post[x\exp]
• wp(skip, post) = post
• wp(A;B , post) = wp(A, wp(B, post))
• wp(if b then A else B) = b ⇒ wp(A, post) ∧ ¬b ⇒ wp(B, post)
• wp(while b do A, post) = ∃ k ∈ N.P_k
  • P₀ = ¬b ∧ post
  • P_i+1 = b ∧ wp(A, P_i), i≥0

—-

Suite de Raffinement de programmes : Raffinement de Programmes