An Axiomatic Semantics for Data-Parallel Computation

Proof rules for both directly and indirectly indexed data-parallel array assignment are presented. Consequently, the correctness of two programs, (i) a representation of Cannon’s algorithm and (ii) sparse matrix-vector multiplication, are established by application of the rules.

Content

Author and article information

Contributors

A. Stewart

Conference

Publication date: September 1997

Publication date (Print): September 1997

Pages: 1-7

Affiliations

[0001]Department of Computer Science, The Queen's University of Belfast

Belfast BT7 1NN

Article

DOI: 10.14236/ewic/FM1997.13

SO-VID: 9879e243-574a-4174-9b37-c38544b8d13c

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Proceedings of the 1st Irish Workshop on Formal Methods

Conference acronym: FM

Conference number: 1

Conference location: Dublin

Conference date: 3-4 July 1997

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Irish Workshop on Formal Methods

History

Product

1477-9358 BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/FM1997.13

Self URI (journal page): https://ewic.bcs.org/

Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

An Axiomatic Semantics for Data-Parallel Computation

Abstract