Theory

This software is based on the UNITY theory, a subset of temporal logic. You develop your program by thinking about a computation in the following way: repeatedly execute any one action, chosen nondeterministically, from a set of actions. Thinking about your program in this way simplifies design.

You reason about program correctness using the following model of computation. A system is a set of agents. Associated with each agent is an action which changes the state of the agent's variables; these variables may be local to the agent or shared with other agents. The variables may be streams or any data type. Computation proceeds by repeatedly selecting any one agent nondeterministically and executing the action of that agent. The selection of agents is fair in the sense that every agent is selected eventually. The examples show how to reason about program correctness and how to map programs to computing networks with threads and processes.

Though we reason about the correctness of our programs assuming that at any point only one agent is executing an action, in practice many agents in many threads and processes may execute concurrently. We separate the concerns of the correctness of our program - the network of agents - from concerns about the performance of our program: how the agent network is mapped onto threads, processes and computers.

Many people have contributed, and continue to contribute, to the theory of UNITY; see, for example, Paulson, Sanders, Rao, Charpentier, Andersen.