Correctness and expressiveness
查看 Markdown本节回答关于 Dex 的两个问题。
- 表达能力（expressiveness）：Dex 能否表达你需要的程序？
- 正确性（correctness）：进程、机器或网络出故障时，Dex 是否仍然正确？
表达能力
表达能力证明说明：一门带线程、锁、Timer 和取消的小型并发语言中，任何程序都能写成行为相同的 Dex Flow。证明的每一步都由计算机检查。完整论证见论文。
Workflow Patterns 评估按 43 个 control-flow Workflow Patterns 为 Dex 评级。研究者用这些模式比较各种 workflow 语言和引擎。每个评级都配有可运行的示例和集成测试。
正确性
Step 的保证说明 Step 方法失败或重复运行时 Dex 的承诺。
故障透明性证明覆盖 server 崩溃、备用 server 接管、重试、Dex 放弃后仍在运行的 Worker，以及重复的结果。这些故障只会带来重复的外部副作用：去掉它们，剩下的就是这个 Flow 在没有故障时能产生的事件序列。对公平的运行，结局也不变。证明的页面列出了它的条件，例如只覆盖 SYNC 方法、重试不会用完。这个证明同样经计算机检查，完整论证见同一篇论文。
两个证明合起来，覆盖那门小型并发语言中每个格式良好的程序。这样的程序在 Dex 上产生的是一次无故障运行的事件，只是外部副作用可能重复，重复也可能来得很晚。这对你的代码意味着什么说明怎样让重复变得安全。