Proofs by annotations for a simple data-parallel language - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1995

Proofs by annotations for a simple data-parallel language

(1) , (1)
1

Résumé

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.
Fichier principal
Vignette du fichier
RR1995-08.pdf (286.1 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02102026 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02102026 , version 1

Citer

Luc Bougé, David Cachera. Proofs by annotations for a simple data-parallel language. [Research Report] LIP RR-1995-08, Laboratoire de l'informatique du parallélisme. 1995, 2+19p. ⟨hal-02102026⟩
8 Consultations
15 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More