On the Expressivity of a Weakest Precondition Calculus for a Simple Data-Parallel Programming Language
Luc Bougé, Yann Le Guyadec, Gil Utard, Bernard Virot · 1994
We present a weakest preconditions calculus `a la Dijkstra for a small common kernel of existing data-parallel languages. We use two-part assertions, where the current extent of parallelism is specified by a separate boolean vector expression. Our main contribution is concerned with the conditioning construct where which modifies the current extent of parallelism. We prove that the weakest (strict) preconditions of a where block is definable by an assertion as soon as its body is. We show that this is not the case with its weakest liberal preconditions. This sheds a new light on the deep semantic nature of the data-parallel conditioning construct. Keywords: Concurrent Programming; Specifying and Verifying and Reasoning about Programs; Semantics of Programming Languages; Data-Parallel Languages; Proof System; Hoare Logic; Weakest Preconditions. Citation: This work has been submitted for presentation at the ConPar'94--VAPP VI Conference, Linz, Austria, September 6--8, 1994. LIP, ENS ...