Les principes essentiels d'une méthodologie nouvelle pour la synthèse de programmes à partir de spécifications formelles : CM-construction des formules atomiques
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
One way to obtain a program from its specification is to prove an existentially quantified theorem using mathematical induction and extracting an algorithm from the proof. This is known as the Deductive Approach in Program Synthesis from formal specifications. Here, the goal is to find a program Prog from its "specification": For a given input vector x satisfying an input condition IC, the goal is to find an output vector z satisfying a given input-output relation IOR(x, z). Hence, specifications can be considered as formula of the form "for any x verifying IC(x) there exists z such that IOR(x, z) holds". This last formula is called the Specification Theorem (ST). We develop here a method for proving STs, called Constructive Matching (CM). The main feature of this method is that it decomposes proving theorems into (conditional) equations-like subproblems that are either directly solved or can be represented as theorems. These new theorems may then be solved in the same way. With respect to the equation solving (unification, narrowing) this method offers an interesting solution for axiomatic theories concerning a special kind of recursive abstract data types. This is due to the fact that if the implemented (loop-free, non complete) matching algorithm does not find the necessary solutions, a new equational theorem can be formulated and a recursive solution obtained. The system called PRECOMAS (PROOFS Educed by constructive Matching for synthesis) is an implementation of our method.
Abstract FR:
Pour obtenir un programme à partir de sa spécification formelle on peut démontrer un théorème contenant des quantificateurs existentiels. Cette approche est appelée "L'approche déductive pour la synthèse de programmes à partir de spécifications". A partir d'un vecteur x en entrée, on cherche un vecteur z en sortie tel que la relation d'entrées-sorties ESR(x,z) soit vérifiée dès que la précondition P(x) l'est. Ainsi, une spécification peut être exprimée de la manière suivante: "Pour chaque x qui vérifie la précondition P(x), on peut trouver z qui vérifie ESR(x,z)". La dernière formule exprimée formellement est un théorème à démontrer et s'appelle le Théorème de Spécification (TS). Nous proposons dans le cadre de cette thèse une méthode pour la démonstration de TS. Cette méthode, appelée "Appariement Constructif' (Constructive Matching), décompose la démonstration d'un théorème donné en sous-problèmes de style équationel, qui sont résolus directement ou bien en les traitant comme les nouveaux théorèmes à prouver. Soit ces théorèmes sont prouvés de manière analogue, soit ils expliquent pourquoi la démonstration originale a échouée. Par rapport à la résolution d'équations (unification, sur-réduction), cette approche propose ainsi une solution non étudiée dans les travaux existants: aborder les problèmes dus à l'incomplétude des outils comme les nouveaux théorèmes (équationels) à démontrer. Notre système PRECOMAS (PROOFS EDUCED by constructive matching for. Synthesis) incarne cette méthode. En conséquence, l'idée principale de l'implémentation de ce système est d'avoir un outil robuste, simple sans être trivial, qui soit facile à utiliser. Il existe depuis longtemps des recherches sur l'automatisation de la transformation de spécifications en algorithmes. Notre système a ceci de particulier que l'utilisateur est conduit par le programme, et non l'inverse.