A Proof System for a Simple Data-Parallel Programming Language

We describe a small kernel language which encapsulates the semantic features of data-parallel control constructs as found in modern data-parallel languages. We give it a denotational semantics, and describe an assertional proof system in the style of Hoare's logic. Our contribution is to use two-part assertions, where the current extent of parallelism is specified using a separate boolean vector expression. The applicability of the proof system is demonstrated through an example. Keywords: Concurrent Programming; Specifying and Verifying and Reasoning about Programs; Semantics of Programming Languages; Data-Parallel Languages; Proof System; Hoare Logic. R'esum'e Nous d'ecrivons un langage minimal qui capture la s'emantique des structures de controle des langages data-parall`eles. Nous d'efinissons une s'emantique d'enotationnelle, et nous d'ecrivons un syst`eme de preuve de programmes par assertions selon la m'ethode axiomatique de Hoare. Notre syst`eme se distingue par l..