Axiom-Based Transformations: Optimisation and Testing

Anya Helene Bagge and Magne Haveraaen

Citation:

Anya Helene Bagge and Magne Haveraaen. Axiom-Based Transformations: Optimisation and Testing. In Jurgen J. Vinju and Adrian Johnstone, editor(s), Proceedings of the Eighth Workshop on Language Descriptions, Tools and Applications (LDTA 2008), volume 238 of Electronic Notes in Theoretical Computer Science, pages 17–33. Elsevier, 2009.

Workshop:

Eighth Workshop on Language Descriptions, Tools and Applications (LDTA 2008), Budapest, Hungary, 2008, proceedings pp.17–33

Journal:

Electronic Notes in Theoretical Computer Science 238(5):17–33, 2009

Paper Links:

[doi] [pdf]

Abstract:

Programmers typically have knowledge about properties of their programs that aren't explicitly expressed in the code – properties that may be very useful for, e.g., compiler optimisation and automated testing. Although such information is sometimes written down in a formal or informal specification, it is generally not accessible to compilers and other tools. However, using the idea of concepts and axioms in the upcoming C++ standard, we may embed axioms with program code. In this paper, we sketch how such axioms can be interpreted as rewrite rules and test oracles. Rewrite rules together with user-defined transformation strategies allow us to implement program or library-specific optimisations.

BibTeX:

@InProceedings{bagge-haveraaen-ldta08-axioms,
  title = {Axiom-Based Transformations: Optimisation and Testing},
  author = {Anya Helene Bagge and Magne Haveraaen},
  year = {2009},
  booktitle = {Proceedings of the Eighth Workshop on Language Descriptions, Tools and Applications (LDTA 2008)},
  editor = {Jurgen J. Vinju and Adrian Johnstone},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {238},
  issue = {5},
  pages = {17--33},
  publisher = {Elsevier},
  doi = {10.1016/j.entcs.2009.09.038},
  issn = {1571-0661},
  location = {Budapest, Hungary},
  url = {http://www.ii.uib.no/~anya/papers/bagge-haveraaen-ldta08-axioms.html},
  pdf = {http://www.ii.uib.no/~anya/papers/bagge-haveraaen-ldta08-axioms.pdf},
}

Copyright:

Copyright © 2009 Elsevier. This is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. The definitive version can be downloaded from Elsevier.