5.1 内存的接口 本节通过一个规范表示接口,不涉及实现,也即不涉及判断真假的具体公式。 首先选择抽象的层级,第二章把“发送”操作用三个变量( val 、 rdy 、 ack )进行描述,并把 val 和 rdy 同时更改表示为一个原子操作。本章把“发送”操作用一个变量进行描述: val 。 接口试图规定“发送”操作是某一类 动作 ,这需要描述怎样的 动作 是符合本接口的,类似于在“函数是一等公民”的编程语言中描述函数。但 TLA+ 只能把 CONSTANT 、 VARIABLE 定义的变量作为模块的参数,而不能把 动作 定义的公式作为模块的参数。作为替代,TLA+ 中可以定义运算符以达到这个目的。把 动作 涉及的 N 个变量列举出来,定义一个 N 元运算符 CONSTANTS operator_as_action(_, _, _, _) 即可。 运算符的返回值不限定类型,而 动作 是一个公式,返回值是布尔型,所以还需要一个表示类型的假设 ASSUME \A p1, p2, p3, p4 : operator_as_action(p1, p2, p3, p4) \in BOOLEAN 在学习了需要的语法知识后,我们可以定义内存的规范了。 -------------------------- MODULE MemoryInterface --------------------------- VARIABLE memInt \* represent memory CONSTANTS Send(_, _, _, _), Reply(_, _, _, _), InitMemInt, \* set of possible initial values of memInt Proc, \* set of processor identiers Adr, \* set of memory addresses Val \* se...
评论
发表评论