Verification of an Optimisation Algorithm of Stack Machine in Functional Programming Languages
Guanhua He · 2006
Software verification is a significant part of software engineering which is used to ensure that the programs meet their specification and deliver the functionality expected by the users. Pure functional programs can be directly verified by tools. This dissertation focuses on implementing an op-timisation algorithm of stack machine in functional program languages, and verifying its correctness with two verification tools, QuickCheck and HOL Light. QuickCheck is used for testing and HOL-Light is used for proof. The optimisation algorithm transfers the instruction code to replace loads and stores with stack manipulation to reduce the memory accesses. The correct-ness of the optimisation is verified by showing the code before a transfor-mation is semantically equivalent to the transformed code. The verification method is generalised, which is useful for further verifications of stack algo-rithms. iDeclaration I declare that this thesis was composed by myself, that the work con-tained herein is my own except where explicitly stated otherwise in the text, and that this work has not been submitted for any other degree or profes-sional qualification except as specified. (Guanhua He) ii