Proofs by annotations for a simple data-parallel language
| Autor: | Luc Bougé, David Cachera |
|---|---|
| Přispěvatelé: | Laboratoire de l'Informatique du Parallélisme (LIP), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Laboratoire de l'informatique du parallélisme, École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL) |
| Jazyk: | angličtina |
| Rok vydání: | 1995 |
| Předmět: |
Weakest Preconditions
Programmation parallèle Proof System Concurrent Programming Specifying and Verifying and Reasoning about Programs Hoare Logic Système de preuve Sémantique des langages de programmation Logique de hoare Semantics of Programming Languages Plus faibles préconditions Spécification et validation de programmes [INFO]Computer Science [cs] Langages data-parallèles Data-Parallel Languages |
| Zdroj: | [Research Report] LIP RR-1995-08, Laboratoire de l'informatique du parallélisme. 1995, 2+19p HAL |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|