MAÎTRISE INFORMATIQUE Option PROGRAMMATION

Module Projet année 2000-01
PROGRAMMATION


Système d'aide au développement de programmes par raffinement I


Sujet proposé par : Pascal MANOURY (Pascal.Manoury@pps.jussieu.fr)

Objectif

Concevoir et développer un outil permettant la construction progressive du texte d'un programme par application de règles de raffinement à partir de sa spécification en terme de pré et post condition.

Description

On peut spécifier le résultat attendu d'un composant logiciel par un couple de formules logique décrivant les conditions d'initiales d'utilisation d'un programme (préconditions) et l'état final des variables manipulées par le programme (postconditions).

Les règles de raffinements permettent de transformer une spécification en suite d'instructions réalisant un calcul permettant de passer des conditions initiales aux conditions finales. La spécification initiale est purement logique, les étapes intermédiaires mélange des formules logiques et des constructions algorithmiques (structures de contrôle impératives) la "spécification" finale ne contient plus que des instructions exécutables.

Cahier des charges

Le système envisagé devra permettre d'engendrer des programmes pour un langage impératif élémentaire : affectation, séquence, conditionnelle, boucle "tant-que". Outre les entiers et les booléens, le langage visé doit savoir traiter les tableaux.
Le langage logique de spécification est un calcul des prédicats du premier ordre que l'on enrichira des constantes d'individus et de prédicats nécessaires.
Autant que possible, on prendra soin d'obtenir une syntaxe pas trop lourde pour le langage de spécification en utilisant les ressources des outils lex et yacc.

Outre le langage, le système offrira à l'utilisateur une série de commande lui permettant de raffiner une spécification par utilisation des règles vues en cours.
Le système offrira, au minimum, une interface utilisateur sous forme de boucle d'interaction. Les commandes essentielles seront : - initialiser la construction d'un programme en donnant sa spécification initiale; - appliquer une règle de raffinement en invocant une commande accompagnée de ses éventuels arguments, le système affiche alors le ou les résultats de l'application sur lesquelles on réitère le processus de raffinement.
Une session de raffinement pourrait être (suggestion de présentation) : 

()> Goal [x=N and y=M, x=M and y=N].
()> Var z.
 new goal : {Var z . [x=N and y=M, y=N and x=M] }
 subgoal 0 {Var z . [x=N and y=M, y=N and x=M] }
(0)> Seq (z=N and y=M).
 new goal : {Var z . [x=N and y=M, z=N and y=M] ; 
                     [z=N and y=M, y=N and x=M] }

 subgoal 1 [x=N and y=M, z=N and y=M]
 subgoal 2 [z=N and y=M, y=N and x=M]
(1)> Aff z (x).
 new goal : {Var z . z := x ; 
                     [z=N and y=M, y=N and x=M] }
 subgoal 2 [z=N and y=M, y=N and x=M]
(2)> Seq (z=N and x=M).
 new goal : {Var z . z := x ; 
                     [z=N and y=M, z=N and x=M] ; 
                     [z=N and x=M, y=N and x=M] }
 subgoal 2.1 [z=N and y=M, z=N and x=M]
 subgoal 2.2 [z=N and x=M, y=N and x=M]
(2.1)> Aff x (y).
 new goal : {Var z . z := x ; 
                     x := y ;
                     [z=N and x=M, y=N and x=M] }
 subgoal 2.2 [z=N and x=M, y=N and x=M]
(2.2)> Aff y (z).
 program : {Var z . z := x ; 
                    x := y ;
		    y := z }
()>

L'auteur du projet verra d'un oeil extrèment favorables que les réalisateurs du projet proposent des règles de raffinements plus riches que celles de base vues en cours. On peut obtenir de telles macros règles par combinaison des règles de base.

Documents

notes de cours de l'auteur du projet (module SCL).

Réalisation

La définition du langage et se sa syntaxe, les algorithmes de vérification d'application des règles, la conception du mécanisme des boucles d'interaction offrent matière à réflexion et à implantation pour un trinôme.