Details

Autor(en) / Beteiligte

• Bougé, Luc
• Cachera, David
• Ali, Khayri
• Magnusson, Peter
• Haridi, Seif

Titel

On the completeness of a proof system for a simple data-parallel programming language (extended abstract)

Ist Teil von

• EURO-PAR '95 Parallel Processing, 2005, p.143-154

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

2005

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• We prove the completeness of an assertional proof system for a simple loop-free data-parallel language. This proof system is based on two-part assertions, where the predicate on the current value of variables is separated from the specification of the current extent of parallelism. The proof is based on a Weakest Precondition (WP) calculus. In contrast with the case of usual scalar languages, not all WP can be defined by an assertion. Yet, partial definability suffices to prove the completeness thanks to the introduction of hidden variables in assertions. The case of data-parallel programs with loops is briefly discussed in the conclusion.