卢本伟是谁 ？

-
“我卢本伟没有开挂没有开挂没开挂，我的背包连着弹夹连着弹夹连弹夹”

然后推荐一个视频《穷开挂》

评论

发表评论

此博客中的热门博文

Specifying Systems 第五章笔记

-
图片
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...
阅读全文

Specifying Systems 第四章笔记

-
图片
本章介绍一个先进先出 FIFO 系统。 4.1 内部结构的规范 一个 FIFO 队列内部是一个缓冲区，对外提供单个消息的入队与出队接口。对于外部接口，TLA+ 可以复用之前的模块，这类似于面向对象编程中实例的概念。我们复用上一章的模块 Channel InChan == INSTANCE Channel WITH Data <- Message, chan <- in InChan 现在是一个 Channel ，除了 Data 和 chan 通过相应的新标识符访问，其余标识符（以及运算符）通过 InChan!symbol 访问。 缓冲区用 TLA+ 的内置数据结构 Sequences 进行表示。 Sequences 表示一个有限序列，字面量用元组表示，并有如下的与之相关的标识符： Seq(S) 表示 S 集合能组成的所有有限序列。 Head(S) 、 Tail(S) 表示序列的首元素及剩余序列。 Append(S) 、 S \o T 表示序列与元素、另一个序列连接。 Len(S) 表示序列的长度。 了解上述语法后，可以把 FIFO 描述为三个组件：依次相连的入队接口、内部先进先出缓冲区、出队接口。FIFO 的状态转移将由相连两组件各自的状态转移以及两组件交互组成。 4.2 实例化的细节 与 EXTENDS 不同，实例化需要导入的所有符号（主要是 CONSTANT 、 VARIABLE 等关键词定义的标识符）都指定本模块中对应标识符。有以下几个方面需要注意。 4.2.1 实例化即替换 TLA+ 的实例化是进行表达式展开和替换。为了满足语法，原模块替换完成后，所有符号在本模块中都要有定义，这可以通过 EXTENDS 引入运算符等符号以及使用 <- 为原模块未匹配的符号指定本模块的标识符、表达式等符号来满足。 4.2.2 实例化的参数化 实例化时可以包含参数，即 InChan == INSTANCE Channel WITH Data <- Message, chan <- in OutChan == INSTANCE Channel WITH Data <- Message, chan <- out 可以使用 Chan(ch) ...
阅读全文