Preuve De Propriété D’atteignabilité Par raffinement

Preuve De Propriété D’atteignabilité Par raffinement

 Le raffinement B

Le raffinement constitue un principe fondamental de développement d’applications sui vant la méthode B. Il permet une construction graduelle et progressive d’un système depuis sa spécification abstraite initiale jusqu’á la génération de code exécutable en introduisant, étape par étape, les structures de données et de contrôle du langage cible choisi. En B, on distingue les deux types de raffinement suivants :– Raffinement de données : il consiste á remplacer une donnée abstraite D par une donnée plus concrète D′.

Dans ce cas, un prédicat, appelé invariant de collage établissant la relation entre D et D′, est défini dans la clause INVARIANT du composant raffiné.– Raffinement de substitutions : il consiste á remplacer une substitution S par une substitution plus concrète S′. Notons qu’un raffinement de données donne lieu au raffinement de substitutions afin que celles-ci soient ré-exprimées en fonction du nouvel espace de données.

Dans le cadre de notre travail, nous utilisons exclusivement le raffinement de substitutions car l’espace des données est toujours conservé. Le développement progressif de système par raffinement est basé sur la propriété de tran sitivité suivante : 72 Définition 1 (Propriété de transitivité) Soient S1, S2 et S3 trois substitutions. Si S2 raf f ine S1 et S3 raffine S2 alors S1 est raffinée par S3 : S1 ⊑ S2 ∧S2 ⊑S3 ⇒S1 ⊑S3

Comme nous le verrons plus loin, la correction de chaque étape de raffinement est vérifiée par la génération d’obligations de preuve qui ont pour but de montrer que la spécification concrète ne contredit pas la spécification abstraite et préserve donc toutes ses propriétés. De proche en proche, nous prouvons ainsi la correction du code obtenu. Dans [21], Morgan a proposé un ensemble de règles de raffinement de spécifications permettant la génération progressive de programmes á partir d’une spécification initiale.

Selon Morgan, une spécification, représentée par w : [pre,post], désigne tout programme s’exécutant depuis un état initial vérifiant pre et terminant dans un état vérifiant post tout en modifiant les variables w. Dans le but d’alléger la notation de Morgan, nous représentons une spécification par spec(ψ, φ) qui agit implicitement sur l’ensemble des variables de la spécification. Le paragraphe suivant introduit les règles de raffinement définies par Morgan pour la génération de programmes á partir de spécifications.

Règles de raffinement de Morgan

Dans cette section, nous présentons trois règles de raffinement introduites par Mor gan. Nous restreignons notre présentation á ces règles utiles pour la preuve de propriété d’atteignabilité objectif de ce chapitre. 

Raffinement par une substitution

Cette règle permet de raffiner une spécification spec(pre, post) par une substitution S : Spec(pre,post) ⊑ S (4.1) Pour prouver un tel raffinement, nous devons montrer que si la substitution S s’exécute á 73 partir d’un état qui satisfait pre alors elle terminera dans un état qui vérifie post. Formel lement : Spec(pre,post) ⊑ S ⇔ (pre ⇒ [S]post)

Raffinement par décomposition séquentielle (4.2)

Cette règle raffine une spécification par la composition séquentielle de deux sous spécifications permettant ainsi de mieux gérer la complexité de la spécification initiale. Une spécification spec(pre, post) est donc raffinée par deux sous-spécifications spec(pre, P1) et spec(P2, post) mises en séquence comme suit : Spec(pre,post) ⊑ Spec(pre,P1);Spec(P2,post) (4.3) Pour prouver un tel raffinement, nous utilisons la notion de la plus faible précondition et montrons que : Spec(pre,post) ⊑ Spec(pre,P1);Spec(P2,post) ⇔ pre ⇒ [Spec(pre,P1)]([Spec(P2,post)]post)