佚名

共享对象的规范

规范（Specification）

  • 规范的例子
    • 不同开发者，开发同一软件 –> 开发文档
    • 不同用户，使用同一软件 –> 使用文档
    • 不同软件，调用同一个库 –> 应用程序接口
    • 不同应用程序，相互通信 –> 通信协议
  • 规范应该具有如下性质
    • 严格性（Rigor）
    • 抽象性（Abstraction）
    • 简洁性（Simplicity）

抽象数据类型

  • 抽象数据类型（Abstract Data Type，ADT）类似于有限自动机和正则表达式中的确定有限自动机（Deterministic Finite Automaton，DFA）
    • A为输入字母表
    • B为输出字母表
    • Z为状态集，\zeta_0 \in Z为初态
    • \tau: Z \times A \to Z为转移映射
    • \delta: Z \times A \to B为输出映射
  • 一个简单的数据库（Database）应用
    • 用集合来存储元素
    • 插入（Insert）元素、删除（Delete）元素
    • 一次性读取（Read）所有元素
    • 由于数据库存储的元素有限，故我们考虑幂集中的有限集合\mathscr{P}_{< \infty}(X)
  • （ADT）集合
    • A = \cup_{x \in X} \{ Insert(x), Delete(x), Read \}
    • B = \mathscr{P}_{< \infty}(X) \cup \{ \perp \}
    • Z = \mathscr{P}_{< \infty}(X)，\zeta_0 = \emptyset
    • \tau: Z \times A \to Z
      • (\zeta, Insert(x)) \mapsto \zeta \cup \{ x \}
      • (\zeta, Delete(x)) \mapsto \zeta - \{ x \}
      • (\zeta, Read) \mapsto \zeta
    • \delta: Z \times A \to B
      • (\zeta, Insert(x)) \mapsto \perp
      • (\zeta, Delete(x)) \mapsto \perp
      • (\zeta, Read) \mapsto \zeta
  • 一个简单的即时消息（Instant Message，IM）应用
    • 用大小为k的滑动窗口来表示屏幕上显示的消息
    • 消息从旧到新显示，最多为k条
    • 发送消息为写（Write），显示消息为读（Read）
  • （ADT）大小为k的滑动窗口
    • A = \cup_{x \in X} \{ Write(x), Read \}
    • B = X^k \cup \{ \perp \}
    • Z = X^k，\zeta_0 = (x_0, \ldots, x_0)
    • \tau: Z \times A \to Z
      • ((x_1, \ldots, x_k), Write(x)) \mapsto (x_2, \ldots, x_k, x)
      • ((x_1, \ldots, x_k), Read) \mapsto (x_1, \ldots, x_k)
    • \delta: Z \times A \to B
      • ((x_1, \ldots, x_k), Write(x)) \mapsto \perp
      • ((x_1, \ldots, x_k), Read) \mapsto (x_1, \ldots, x_k)

更新、查询

  • ADT有两种基本操作——更新（Update）、查询（Query）
    • （ADT）集合
      • Insert、Delete为更新
      • Read为查询
    • （ADT）大小为k的滑动窗口
      • Write为更新
      • Read为查询
  • 一般来说，我们希望更新、查询是分离的。然而，队列（Queue）的Pop既是更新，也是查询，所以我们需要将Pop分解为Remove、Head