Preuves de Propriétés de Classes de Programmes par Dérivation Systématique de Jeux de Test
Résumé
The problem addressed in this thesis concerns the automatic production of test data to prove properties of programs. We stand halfway between the area of testing and program verification. Work in the area of testing have led to semi-automatic tools easy to use, but which are based on assumptions difficult to verify in practice. In the field of verification, tools based on formal methods have been developed, but require an expert user in the proof techniques used by the tool. This is due to the problems of undecidability generated by the power of formalisms treated. The thesis presented here is that it is possible to develop automated formal methods to prove properties of programs, provided formalisms considered are restricted. Our main contribution is a new approach to program verification, including testing techniques and static analysis. We propose a formal method for generating complete finite test sets to prove that a program satisfies a given property. This method uses the program text and property, which must belong to certain classes of programs (or properties). These classes are represented by hierarchies of patterns, which can be viewed as modeling assumptions test. Any program belonging to one of our patterns and passing the test set satisfies the property successfully tested. For a given property, our method is completely automatic and does not require any particular skill of the user. We have implemented this method in a prototype (processing a restricted functional language), in the case of properties in terms of lengths of lists.
Le problème abordé dans cette thèse concerne la productionautomatique de données de test permettant de prouver des propriétés de programmes. Nous nous situons ainsi à mi-chemin entre le domaine du test et celui de la vérification de programmes. Les travaux dans le domaine du test ont conduit à des outils semi-automatiques d'utilisation simple, mais qui reposent sur des hypothèses difficilement vérifiables en pratique. Dans le domaine de la vérification, des outils basés sur des méthodes formelles ont été développés, mais ils nécessitent un utilisateur expert dans les techniques de preuve utilisées par l'outil. Cette situation est due aux problèmes d'indécidabilité engendrés par la puissance des formalismes traités. La thèse que nous présentons est qu'il est possible de développer des méthodes formelles automatiques pour prouver des propriétés de programmes, à condition de considérer des formalismes restreints. Notre principale contribution est une nouvelle approche pour la vérification de programmes, intégrant les techniques de test et d'analyse statique. Nous proposons une méthode formelle de génération de jeux de test finis complets permettant de prouver qu'un programme vérifie une propriété donnée. Cette méthode utilise le texte du programme et de la propriété, qui doivent appartenir à certaines classes de programmes (ou de propriétés). Ces classes sont représentées par des hiérarchies de schémas, qui peuvent être vues comme modélisant des hypothèses de test. Tout programme appartenant à un de nos schémas et passant le jeu de test avec succès vérifie la propriété testée. Pour une propriété donnée, notre méthode est complètement automatique et ne nécessite donc aucune compétence particulière de l'utilisateur. Nous avons implanté cette méthode dans un prototype (traitant un langage fonctionnel restreint), pour le cas de propriétés s'exprimant en termes de longueurs de listes.
Loading...