本节介绍了FIFO缓冲区规约,重点说明了如何引入其他模块的实例,例如
InChan≜INSTANCE Channel WITH Data←Message,chan←in还顺带介绍了
Sequences模块的几个运算符。
FIFO规约首先
Extends了模块
Naturals和
Sequences。
Sequences模块定义有限序列上的运算。我们把一个有限序列表示成一个元组,所以三个数3,2,1的序列是三元组
⟨3,2,1⟩,
Sequences模块对序列定义了如下运算符:
-
Seq(S) 集合
S中任意元素组成的所有序列的集合,例如,
⟨3,7⟩是
Seq(Nat)的一个元素。
-
Head(s) 序列
s的第一个元素。例如,
Head(⟨3,7⟩) = 3。
-
Tails(s) 序列s的尾部,它由去掉头部的序列s组成。例如,
Tail(⟨3,7⟩)=⟨7⟩。
-
Append(s,e) 将元素e附加到
s的尾部得到的序列,例如,
Append(⟨3,7⟩,3)=⟨3.7.3⟩
-
s∘t 将序列s和t串联起来得到的序列,例如
⟨3,7⟩∘⟨3⟩=⟨3,7,3⟩。(我们在ASCIl中输入o作为\o。)
-
Len(s) 序列
s的长度,例如,
Len(⟨3,7⟩)=2
FIFO规约继续声明常量
Message,其表示所有可发送消息的集合,接下来声明三个变量:
in和
out代表通道,第三个变量
q代表缓冲消息队列。
q的值是发送方已发送但接收方尚未接收的消息序列。(第4.3节对这个额外变量
q有更多说明)。
我们希望使用
Channel模块中的定义来指定
in和
out通道上的操作。这需要该模块的两个实例:在其中一个实例中,
Channel模块的变量
chan替换为当前模块的变量
in, 另一个实例的
chan替换为
out。在这两个实例中,
Channel模块的常量
Data被替换为
Message。我们使用下列语句描述第一个实例:
InChan≜INSTANCE Channel WITH Data←Message,chan←in
定义在模块
Channel中的任意符号
σ,与定义在当前模块中的
InChan!σ有相同的含义,只除了
Message代替的
Data和
in代替的
chan。例如下列语句定义
InChan!TypeInvariant等于
in∈[val:Message,rdy:{0,1},ack:{0,1}]
(该语句没有定义
InChan!Data,是因为
Data是在
Channel模块中声明而不是定义的。)我们用类似的语句引入
Channle模块的第二个实例:
OutChan≜INSTANCE Channel WITH Data←Message,chan←out
in和
out通道的初始状态由
InChan!Init和
OutChan!Init指定。最初,没有消息被发送或接收,所以
q等于空序列。空序列是0元组(只有一个,它被写为
⟨⟩)。所以我们将初始谓词定义为:
Init≜∧InChan!Init∧OutChan!Init∧q=⟨⟩
接下来定义类型不变量。
in和
out的类型不变量来自
Channle模块,而
q的类型是消息的有限序列的集合。因此,FIFO规约的类型不变量是
TypeInvariant≜∧InChan!TypeInvariant∧OutChan!TypeInvariant∧q∈Seq(Message)
下一状态动作所允许的四种非重叠步骤由下列四个动作来描述:
-
SSend(msg) 发送方在
in通道上发送消息;
-
BufRcv 缓冲区从
in通道上接收消息,并将之放入
q的队尾;
-
BufSend 缓冲区在
out通道发送
q的队首并将之从
q删除;
-
RRcv 接收方从
out通道接收消息;
这些动作的定义,以及规约的其余部分,见下一页图4.1的模块
InnerFIFO,下文第4.3节解释形容词
Inner。