PROVING DATA-PARALLEL PROGRAMS: A UNIFYING APPROACH
David Cachera, Gil Utard · Parallel Processing Letters · 1996
We define an axiomatic semantics for a common kernel of existing data-parallel languages. We introduce an assertional language which enables us to define a weakest liberal precondition calculus which has the Definability Property, and a proof system (`a la Hoare) which has the Completeness Property. Moreover, our axiomatic semantics integrates two previous works in the definition of proof systems for data-parallel programs. This work sheds a new light on the logical complexity of proving data-parallel programs.