编程的实践理论 第九章 交互

第九章 交互

根据状态的初始值和终止值，我们已经描述了计算。一个状态变量的声明如下：
var x: T· S   =   ∃x, x′: T· S

它说的是一个状态变量有两个数学变量，一个是初始值，一个是终止值。在这个
声明的作用域内，x和x'是在规格S中可用的。当这是一个依赖性的组合时，有
中间的变量值，但是这种中间值对于依赖性的组合的定义是本地化的。
P. Q   =   ∃x′′, y′′, ...·  〈x′, y′, ...→P〉 x′′ y′′ ...  ∧  〈x, y, ...→Q〉 x′′ y′′ ...
考虑  (P. Q)  || R 。 在独立的组合中，在P和Q之间的中间值是隐藏的，
对于 R是不可见的，所以它们不能够用于进程的交互。

一个变量仅是初始值和终止值是可见的，叫做一个边界变量，一个变量的
所有的值都是可见的，叫做交互变量。所以，我们的变量都是边界的变量。
现在我们引入了交互变量，它的中间值对并行进程是可见的。这些变量用于
描述和推理人和计算机之间的交互，还有一个计算过程中的进程之间的交互。

9.0 交互的变量

令记号  ivar x: T· S 声明x为一个类型为T，作用域为S的交互变量。
它的定义如下：
ivar x: T· S   =   ∃x: time→T· S
时间是域的时间，或者是扩展的整数或者是扩展的实数。一个交互的变量
是一个时间的函数。变量x的值在时间t处是x t。

假定a和b是边界变量，x和y是交互变量，t是时间。对于独立的组合，我们
分区了所有的状态变量，边界变量和交互变量。假定 a 和 x 属于P，b和y 
属于Q。
P||Q =   ∃tP, tQ·      〈t′→P〉 tP  ∧  (∀t′′· tP≤t′′≤t′ ⇒ xt′′=x(tP))
∧  〈t′→Q〉 tQ  ∧  (∀t′′· tQ≤t′′≤t′ ⇒ yt′′=y(tQ))
∧  t′ = max tP tQ

新的部分说，当短的进程被完成了，它的交互变量保留不变，直到长的进程完成了。

在如同之前的图，使用相同的进程和变量，赋值语句 x:= a+b+x+y  在进程P中，变量x
赋值为四个变量的和。因为a和x是进程P的变量，它们的值由进程P赋值最新的值，如果
没有进程P给这些变量赋值，这些变量保持初始值。因为b是进程Q的边界变量，它的值
在进程P中可以看到它的初始值，无论Q是否给它赋值。因为y是进程Q中一个交互变量，
它的值在进程P中可以看到，是由进程Q赋值的最新的值，或者是Q没有赋值的初始值，
或者是不知道。因为x是一个交互变量，它的新值在所有的并行的进程中可以看到。
表达式a+b+x+y 是一个有混淆的记号，因为a和b是数值，x和y 是从时间到数值的函数，
数值实际上被赋值为 a+b+xt+yt，但是当上下文清楚时，我们忽略了实际参数t。
我们将相似的写着x' 意味着 xt' ，x''意味着xt''。

ok的定义说边界变量和时间没有改变。所以之前的两个图中，在进程P中，
ok   =   a′=a  ∧  t′=t

当含义是xt'=xt ，因为t'=t, 我们不需要说 x'=x。我们没有提及b和y ,
因为它们不是进程P的变量。

对交互变量的赋值，不能被实例化，因为它是时间来区别它的值。
在一个进程中，当一个边界变量是a和b，交互变量是x和y,

x:= e   = a′=a  ∧  b′=b  ∧  x′=e  ∧  (∀t′′· t≤t′′≤t′ ⇒ y′′=y)
∧ t′ = t+(要求评估和存储  e的时间 )

在对x的赋值其间，交互式变量y保留不变。在赋值期间关于x的值没有说。

如果我们愿意的话，对一个边界变量的赋值可以实例化。如果我们选择了对
时间的计量，我们必须说在赋值期间，所有的交互式变量都保持了不变。

依赖性的组合隐藏了边界变量和时间变量的中间值，只有交互式变量的中间
值是可见的。在边界变量a和b,交互式变量x和y,时间t, 我们定义
P. Q   =   ∃a′′, b′′, t′′·  〈a′, b′, t′→P〉 a′′ b′′ t′′  ∧  〈a, b, t→Q〉 a′′ b′′ t′′

规格定律和推导定律的绝大部分，保留了交互式变量的可加性，但是很可惜的是，
替换定律不再是有效的。

如果P和Q是并行的，它们有不同的变量。再假定边界变量a和交互式变量x是进程P
的变量，边界变量b和交互式变量y是Q进程的变量。在规格P中，输入是a,b,xt,yt'',
条件是 t<=t''<t'。在规格P中，输出是a' 和 xt'' ，规格P是可实现的，条件如下：
∀a, b, X, y, t· ∃a′, x, t′·  P  ∧  t≤t′  ∧  ∀t′′· t<t′′≤t′  ∨  x t′′=X t′′

正如之前的，P必须被满足，没有非减时间，新的部分说，P必须不包括t到t'之间外的
交互式变量。我们不需要知道一个进程的规格的上下文，来检查它的可实现性；变量
b 和 y 仅出现在通用量词之外。

练习448号是一个例子，它有相同的变量，a,b,x,y,t。假定时间是一个扩展的整数，每
一次赋值花费时间 为1.

(x:= 2.  x:= x+y.  x:= x+y) || (y:= 3.  y:= x+y)     x是左边进程的变量，y是右边进程的变量 
                                                                      a在左边进程，b是右边进程
=    (a′=a ∧ xt′=2 ∧ t′=t+1. a′=a ∧ xt′= xt+yt ∧ t′=t+1. a′=a ∧ xt′= xt+yt ∧ t′=t+1)
||  (b′=b ∧ yt′=3 ∧ t′=t+1.  b′=b ∧ yt′= xt+yt ∧ t′=t+1)
=    (a′=a ∧ x(t+1)=2 ∧ x(t+2)= x(t+1)+y(t+1) ∧ x(t+3)= x(t+2)+y(t+2) ∧ t′=t+3)
||  (b′=b ∧ y(t+1)=3 ∧ y(t+2)= x(t+1)+y(t+1) ∧ t′=t+2)
=     a′=a ∧ x(t+1)=2 ∧ x(t+2)= x(t+1)+y(t+1) ∧ x(t+3)= x(t+2)+y(t+2)
∧  b′=b ∧ y(t+1)=3 ∧ y(t+2)= x(t+1)+y(t+1) ∧ y(t+3)=y(t+2) ∧ t′=t+3
=     a′=a ∧ x(t+1)=2 ∧ x(t+2)=5 ∧ x(t+3)=10
∧  b′=b ∧ y(t+1)=3 ∧ y(t+2)=y(t+3)=5 ∧  t′=t+3

因为我们每一个赋值花费时间为1，例子给出了锁步骤的同步的样子。
更加现实的是，不同的赋值花费不同的时间，可能规定了不确定性
的上界和下界。我们决定了时间策略，是确定性还是不确定性，是
离散的还是连续的，定义和理论保持不变。当然了，复杂的时间
导致了非常复杂的表达式，用来描述所有的可能的交互过程。如
果关于可能的行为，我们要知道仅仅是一部分事，而不是所有的事，
我们能用推导来代换方程，弱化了简化目的。编程有其它的方式：
我们开始于一个期望行为的规格，加强了编程的必要性。