We have been describing computation according to the initial values and final values of state
variables. A state variable declaration
var x: T· S = ∃x, x′: T· S
says that a state variable is really two mathematical variables, one for the initial value and one for the
final value. Within the scope of the declaration, x and x′ are available for use in specification S .
There are intermediate values whenever there is a dependent (sequential) composition, but these
intermediate values are local to the definition of dependent composition.
P. Q = ∃x′′, y′′, ...· 〈x′, y′, ...→P〉 x′′ y′′ ... ∧ 〈x, y, ...→Q〉 x′′ y′′ ...
Consider (P. Q) || R . The intermediate values between P and Q are hidden in the dependent
composition, and are not visible to R , so they cannot be used for process interaction.
A variable whose value is visible only initially and finally is called a boundary variable, and a
variable whose value is visible all the time is called an interactive variable. So far our variables have
all been boundary variables. Now we introduce interactive variables whose intermediate values are
visible to parallel processes. These variables can be used to describe and reason about interactions
between people and computers, and between processes, during the course of a computation.
9.0 Interactive Variables
Let the notation ivar x: T· S declare x to be an interactive variable of type T and scope S . It is
defined as follows.
ivar x: T· S = ∃x: time→T· S
where time is the domain of time, usually either the extended integers or the extended reals. An
interactive variable is a function of time. The value of variable x at time t is x t .
Suppose a and b are boundary variables, x and y are interactive variables, and t is time. For
independent composition we partition all the state variables, boundary and interactive. Suppose a
and x belong to P , and b and y belong to Q .
P||Q = ∃tP, tQ·
〈t′→P〉 tP ∧ (∀t′′· tP≤t′′≤t′ ⇒