X-machine

The relation DoSubExpr maps a parse tree containing multiple occurrences of the same expression "x + y ... x + y" into an optimized version with a local variable to store the repeated computation "z := x + y; ... z ... z".

Interest in the X-machine was revived in the late 1980s by Mike Holcombe,[2] who noticed that the model was ideal for software formal specification purposes, because it cleanly separates control flow from processing.

[7] Another variant, the Communicating Stream X-Machine offers a useful testable model for biological processes[8] and future swarm-based satellite systems.

[9] X-machines have been applied to lexical semantics by András Kornai, who models word meaning by `pointed' machines that have one member of the base set X distinguished.

[10] Application to other branches of linguistics, in particular to a contemporary reformulation of Pāṇini were pioneered by Gerard Huet and his co-workers[11][12] The X-machine is rarely encountered in its original form, but underpins several subsequent models of computation.

NASA has recently discussed using a combination of Communicating Stream X-Machines and the process calculus WSCSS in the design and testing of swarm satellite systems.

[9] The earliest variant, the continuous-time Analog X-Machine (AXM), was introduced by Mike Stannett in 1990 as a potentially "super-Turing" model of computation;[13] it is consequently related to work in hypercomputation theory.

As a result, complex software systems may be decomposed into a hierarchy of Stream X-Machines, designed in a top-down way and tested in a bottom-up way.

The first fully formal model of concurrent X-machine composition was proposed in 1999 by Cristina Vertan and Horia Georgescu,[22] based on earlier work on communicating automatata by Philip Bird and Anthony Cowling.

This compositional model was proven equivalent to a standard Stream X-Machine,[24] so leveraging the earlier testing theory developed by Holcombe and Ipate.

Kirill Bogdanov and Anthony Simons developed several variants of the X-machine to model the behaviour of objects in object-oriented systems.

[25] This model differs from the Stream X-Machine approach, in that the monolithic data type X is distributed over, and encapsulated by, several objects, which are serially composed; and systems are driven by method invocations and returns, rather than by inputs and outputs.

Further work in this area concerned adapting the formal testing theory in the context of inheritance, which partitions the state-space of the superclass in extended subclass objects.