K. R. Apt and E. Olderog, Veriication of Sequential and Concurrent Programs. T ext and Monographs in Computer Science, 1990.

L. Boug-e, Y. L. Guyadec, G. Utard, and B. Virot, On the expressivity o f a w eakest preconditions calculus for a simple data-parallel programming language, ConPar'94{VAPP VI, 1994.

L. Boug-e and D. Cachera, On the completeness of a proof system for a simple data-parallel programming language, Research Report, vol.94, issue.42, 1994.

L. Boug-e, Y. L. Guyadec, G. Utard, and B. Virot, A proof system for a simple data-parallel programming language, Proc. of Applications in Parallel and Distributed Computing, vol.10, 1994.

L. Boug-e and J. Levaire, Control structures for data-parallel SIMD languages: semantics and implementation, Future Generation Computing Systems, vol.8, pp.363-378, 1992.

Y. L. Guyadec and B. Virot, Axiomatic semantics of conditioning constructs and non-local control transfers in data-parallel languages, Research Report 94{15, 1994.

, Maspar Parallel Application Language Reference Manual, 1990.

N. Paris, HyperC speciication document, HyperParallel Technologies, 1993.

, Thinking Machine Corporation, Cambridge MA. C programming guide, pp.1-9