Specification, testing and verification of unconventional computations using generalized X-machines

Abstract

There are as yet no fully comprehensive techniques for specifying, verifying and testing unconventional computations. In this paper, we propose a generally applicable and designer-friendly specification strategy based on a generalized variant of Eilenberg’s X-machine model of computation. Our approach, which extends existing approaches to SXM test-based verification, is arguably capable of modelling very general unconventional computations, and would allow implementations to be verified fully against their specifications.

Notes

1 The space is not locally compact. If we wish to include -based computations in the scheme proposed here, we first re-interpret each function in as a partial function in . Since is locally compact, the current analysis can then be applied.

Our research is partially supported under the Royal Society International Exchanges Scheme (ref. IE110369).