表达能力证明
查看 MarkdownDex 有一个经计算机检查的证明，说明它能表达什么。
结论
论文定义了一门小型并发语言。它具备并发编程的常用工具：
- 线程，以及 fork 和 join；
- 共享变量、局部变量，以及可递归的过程；
- 互斥锁（mutex）和条件变量（condition variable）；
- 定时：sleep，以及等待一条消息或超时的 select；
- 取消线程；
- 异常；
- 外部副作用，例如发送一封邮件；
- 程序退出。
结论：这门语言中的每个程序，都能翻译成一个从外部看行为相同的 Dex Flow。确切的条件见论文。
“行为相同”包含两部分。
- 相同的事件。 程序能产生的任何事件序列，Flow 都能产生，反过来也一样。
- 相同的结局。 程序和 Flow 在相同的情况下完成、卡住或一直运行。
“从外部看”指输入、外部副作用和结果。Flow 内部的 Channel 和 Attribute 不算在内。
这对你意味着什么
Dex 没有会阻塞的线程，也没有跨等待持有的锁。一个 Flow 是一组 Step：它们读写 Attribute，发布和消费 Channel 消息，并等待 Timer。所以你可能会担心：有些并发逻辑是不是没法写成 Flow？
这个证明表明：凡是能用上面这些构件写出的并发逻辑，都能写成 Flow。
这个翻译是为证明而做的构造，不是 Dex 附带的编译器。它大致为每条语句使用一个 Step，这不是建模应用的方式。建模你自己的 Flow 时，请参考设计模式。
每个构件如何搭建
| 构件 | Dex 构件 | 相关设计模式 |
|---|---|---|
| 线程 | 一串 Step，通常每条语句一个。wait 用三个 Step，sleep 和带超时的 select 会多一个入口 Step。线程的位置和局部状态放在 Step 输入中传递。任一时刻，一个运行中的线程就是一个活跃的 Step 执行。 | |
| fork | GoToMany 到父线程的下一个 Step 和子线程的第一个 Step。 | |
| join | 结束的线程向自己的 join Channel 发布一条消息，然后返回 DeadEnd。执行 join 的 Step 用 AnyOf 等待这个 Channel 和自己的取消 Channel。 | Await Parallel Steps |
| 互斥锁 | 一个 Channel，在互斥锁空闲时持有一个 token。lock 用 ForOne 等待这个 token，等待者按开始等待的顺序获得服务。unlock 把 token 发布回去。 | Critical Section |
| 条件变量 | 一个 Attribute 保存等待线程的列表，每个等待者有自己的 Channel。wait 把线程加入列表，释放互斥锁，等待自己的 Channel，然后重新获取互斥锁。signal 移除第一个等待者，并向它的 Channel 发布消息。broadcast 对每个等待者都这样做。 | |
| sleep | 一个定时 Step。它的 WaitFor 返回 AnyOf，包含一个 Timer 和线程的取消 Channel。 | |
| 带超时的 select | 同一个定时 Step。它用 AnyOf 等待一个 Timer、输入 Channel 和取消 Channel。只有胜出的 Condition 会消费消息。 | Deferred Choice |
| 取消 | 向被取消线程的取消 Channel 发布一条消息。线程只在本会阻塞的位置看到它。 | |
| 异常 | 处理器栈放在 Step 输入中传递。throw 是一次 GoTo，跳到处理器的 Step。 | |
| 退出或失败 | 带结果的 ForceComplete，或带错误的 ForceFail。 | |
| 外部副作用 | 一个 Execute，它唯一的副作用就是这次外部调用。 |
互斥锁不能用 Attribute 锁实现，因为它只覆盖一个 Step 方法，不覆盖等待。Channel token 可以跨多个 Step 和等待持有。
如何验证
证明用 Lean 证明助手写成，它检查每一步。
故障
这个证明覆盖没有故障的运行。故障透明性证明把它扩展到崩溃、恢复、重试和消息重投。在那个页面列出的条件下，从有故障的运行中去掉重复的外部副作用，剩下的就是一次无故障的运行。两个证明合起来表明：这门语言中格式良好的程序在 Dex 上运行时，产生的是一次无故障运行的事件，只是外部副作用可能重复。
相关证据
Workflow Patterns 评估按 43 个 workflow 模式为 Dex 评级，每个评级都配有可运行的示例和针对真实 server 的测试。这些模式在真实 server 上测试常见情形；证明则覆盖这门语言的每个程序。