Proofs by annotations for a simple data-parallel language

We present a proof outline generation system for a simple data-parallel kernel language called L. We show that proof outlines are equivalent to the sound and complete Hoare logic defined for L in previous papers. Proof outlines for L are very similar to those for usual scalar-like languages. In particular, they can be mechanically generated backwards from the final post-assertion of the program. They appear thus as a valuable basis to implement a validation assistance tool for data-parallel programming.Nous présentons un système pour la génération de schémas de preuve par annotations proof outlines pour un petit noyau de langage à parallélisme de données appelé L. Nous montrons que les schémas de preuve par annotations sont équivalents à la logique de Hoare pour le langage L définie dans les articles précédents. La manipulation des annotations des programmes L est très semblable à celle des langages scalaires habituels de type Pascal. En particulier, les annotations peuvent être générées automatiquement à partir de la post-condition du programme. Cette méthode constitue donc une base formelle intéressante pour l'implémentation d'outils d'aide à la programmation data-parallèle