QuickCheck for Whiley
Author(s). Janice Chin.
Venue. Final Year Project (ENGR489) Thesis, Victoria University of Wellington, 2018.
Abstract. Whiley is a programming language that verifies code using formal specifications to improve software quality. Whiley contains a verifying compiler which can identify common bugs. However, the compiler is limited in its ability to discover bugs and may take a long time to verify large programs. Testing is another approach to find bugs. However, testing Whiley programs requires users to manually write code which can be a valuable but time-consuming process. This report details an automatic test case generation tool developed for Whiley based on an existing tool, QuickCheck. QuickCheck for Whiley has been implemented for random and exhaustive test-case generation with different data types generated. Optimisations were made to the tool by implementing function optimisation and memoisation. The tool was evaluated using several test suites to analyse the performance and ability of the tool to test programs. Several bugs were discovered within the test suites and subsequently fixed.