Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    A Case Study on Proving Transformations Correct: Data-Parallel Conversion

    2nd Irish Workshop on Formal Methods

    Cork, Ireland. 2nd - 3rd July 1998


    S. Fitzpatrick, M. Clint & P. Kilpatrick


    The issue of correctness in the context of a certain style of program transformation is investigated.

    This style is characterised by the fully automated application of large numbers of simple transformation rules to a representation of a functional program (serving as a specification) to produce an equivalent efficient imperative program.

    The simplicity of the transformation rules ensures that the proofs of their correctness are straightforward. A selection of transformations appropriate for use in a particular context are shown to preserve program meaning.

    The transformations convert array operations expressed as the application of a small number of general-purpose functions into applications of a large number of functions which are amenable to efficient implementation on an array processor.


    PDF filePDF Version of this Paper (135kb)