A program optimisation must have two key properties: it must preserve the meaning of programs (correctness) while also making them more efficient (improvement). An optimisation's correctness can often be rigorously proven using formal mathematical methods, but improvement is generally considered harder to prove formally and is thus typically demonstrated with empirical techniques such as benchmarking. The result is a conspicuous ``reasoning gap'' between correctness and efficiency. In this thesis, we focus on a general-purpose optimisation: the worker\slash wrapper transformation. We develop a range of theories for establishing correctness and improvement properties of this transformation that all share a common structure. Our development culminates in a single theory that can be used to reason about both correctness and efficiency in a unified manner, thereby bridging the reasoning gap.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:740658 |
| Date | January 2017 |
| Creators | Hackett, Jennifer L. P. |
| Publisher | University of Nottingham |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://eprints.nottingham.ac.uk/46840/ |
Page generated in 0.0018 seconds