如何看待谷歌 Chrome 浏览器宣布将于 2020 年停止支持 Flash Player? 获取链接 Facebook X Pinterest 电子邮件 其他应用 - 八月 24, 2019 说实话 flash 这种技术几百年前就应该被淘汰了 (小声)只是还有一些古老的网站需要 获取链接 Facebook X Pinterest 电子邮件 其他应用 评论
Follow.is Feed Verification - 十月 12, 2024 This message is used to verify that this feed (feedId:68119418071751680) belongs to me (userId:67570460419266560). Join me in enjoying the next generation information browser https://follow.is. 阅读全文
Specifying Systems 第五章笔记 - 十二月 14, 2019 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 第四章笔记 - 十二月 14, 2019 本章介绍一个先进先出 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) ... 阅读全文
评论
发表评论