SEQUENTIAL-LIKE PROOFS OF DATA-PARALLEL PROGRAMS
Yann Le Guyadec, Bernard Virot · Parallel Processing Letters · 1996
We define a proof system à la Hoare for a common kernel of existing data-parallel languages. It includes conditioning constructs and non-local control transfers such as data-parallel break and continue. Assertions are usual predicates and manipulations of the extent of parallelism are translated into explicit assignments. Therefore, proofs reuse the classical assertional setting of sequential Hoare Logic.