Linguistic Support for Test Development
Lead Research Organisation:
University of Cambridge
Department Name: Computer Science and Technology
Abstract
Computer programs do not preform as reliably as we would like them to. This becomes annually more problematic, as society increasingly relies on computers for business and even safety concerns.Over the last half-century, programming languages have evolved to support better features (e.g. structured programming, object-oriented programming) that encourage clean program design. These improvements aid program reliability.Of course, designing and writing a program is only the first part of building a system; the system then must be tested. While there is a fair degree of theory and practice of testing (program components are tested individually in so-called ``unit tests'', these components are then assembled and whole-system tests are then performed), this procedure is largely informal in that it is largely done by hand, isolated from the design of the software itself.This grant proposal builds on our previous work in testing and in programming language design to argue that software should always be co-developed with its tests, and to do this writing tests must be simplified. This has various advantages. Firstly, expressing the tests in a formalized syntax, directly connected to the program syntax, directs the language to automatically convert the formal specifications into a test suite. Secondly, developing the tests alongside the program increases the likelihood that programmers always update the tests when updating the program -- indeed with the formal specifications we can perform directed analyses, similar to dataflow analysis, to ensure that tests remain exhaustive over updates (according to one of the possible metrics for this).
Organisations
People |
ORCID iD |
| Alan Mycroft (Principal Investigator) |
| Description | Computer programs do not preform as reliably as we would like them to. This becomes annually more problematic, as society increasingly relies on computers for business and even safety concerns. Over the last half-century, programming languages have evolved to support better features (e.g. structured programming, object-oriented programming) that encourage clean program design. These improvements aid program reliability. Of course, designing and writing a program is only the first part of building a system; the system then must be tested. While there is a fair degree of theory and practice of testing (program components are tested individually in so-called ``unit tests'', these components are then assembled, and finally whole-system tests are performed), this procedure is largely informal in that it is largely done by hand, isolated from the design of the software itself. Moreover, tests of whole programs, ``system tests'', are in general much more ad-hoc. The grant premise was that software should always be co-developed with its tests, and to do this writing tests must be simplified. This has various advantages. Firstly, expressing the tests in a formalized syntax, directly connected to the program syntax, directs the language to automatically convert the formal specifications into a test suite. Secondly, developing the tests alongside the program increases the likelihood that programmers always update the tests when updating the program -- indeed with the formal specifications we can perform directed analyses, similar to dataflow analysis, to ensure that tests remain exhaustive over updates (according to one of the possible metrics for this). The main results of the research were: 1. The theoretical connection between unit test specifications and Floyd-Hoare pre- and post-condition verification specifications was developed. This allows tests to be written in a richer language than typical unit tests (including allowing "old(x)" to refer to the value of x before test execution, so that e.g. "x=old(x)+1" can be expressed). 2. An extension (testJava) to Java was designed and implemented based on this idea. It uses transactional-memory-style techniques to support primitives such as "old(x)" and "modifiesOnly()". 3. A methodology was developed to allow unit tests (exploiting their transactional implementation) to be continuously checked during program execution. This allows a unit test suite in our system to become an additional system test suite, monitoring whether program execution diverges from paths anticipated by unit tests. 1. and 2. were foreseen before the grant started, but the insight into 3. occurred during the grant. 3. has temporarily been published as a technical report, and a case for a follow-on grant has been written. |
| Exploitation Route | We believe that developing the notion of "enduring testing" ("system tests from richer unit tests") is worthy of further exploration after the end of the grant. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | Results from our initial paper and ideas combining unit tests with logic and incorporating this into the programming language has been used in a related form within the DrRacket development environment when used by first and second term students in a variety of universities within the United States and one within Germany. This is exposing introductory programmers to the utility of testing and serving as a stepping stone to formal reasoning (using ACL2). |
| First Year Of Impact | 2008 |
| Sector | Education |