Axiomatic Semantics of Data-Parallel Languages; Automatization of Programs Verification - LARA - Libre accès aux rapports scientifiques et techniques
Rapport (Rapport De Recherche) Année : 1993

Axiomatic Semantics of Data-Parallel Languages; Automatization of Programs Verification

Résumé

We give a Hoare-like proof system for the data-parallel language L, and we present an automatic tool to aid program correctness proof. After recalling L's operational semantics, we define an axiomatic semantics. We illustrate proof of L programs with two examples. Then we extend our semantics to weakest precondition, and we deduce techniques for mechanizing program verification from Gordon's verification condition method. We prove its correctness, and we present an implementation of this method in the CENTAUR system.
Nous présentons un système de preuve à la Hoare pour le langage à parallélisme de donnée L, ainsi qu'une automatisation possible de la preuve de programmes; Dans un premier temps nous définissons une sémantique axiomatique de L, après un rappel de sa sémantique opérationnelle. Nous illustrons son application à la preuve de programmes sur deux exemples,dont un non trivial. Ensuite, après avoir étendu notre sémantique aux pré-conditions les plus faibles, nous déduisons une mécanisation de la preuve de programmes inspirée des vérification condition de Gordon. Nous prouvons alors sa correction. Nous présentons enfin son implémentation sous l'atelier sémantique CENTAUR
Fichier principal
Vignette du fichier
RR1993-08.pdf (458.56 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : hal-02101782 , version 1

Citer

V. Mounier, Gil Utard. Axiomatic Semantics of Data-Parallel Languages; Automatization of Programs Verification. [Research Report] LIP RR-1993-08, Laboratoire de l'informatique du parallélisme. 1993, 2+48p. ⟨hal-02101782⟩
18 Consultations
25 Téléchargements

Partager

More