---
title: "Correctness and expressiveness"
description: "本节回答关于 Dex 的两个问题。"
canonical_url: "https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/"
source: "docs/i18n/zh-Hans/docusaurus-plugin-content-docs/current/correctness-and-expressiveness/index.mdx"
locale: "zh-Hans"
---

# Correctness and expressiveness

本节回答关于 Dex 的两个问题。

- **表达能力（expressiveness）**：Dex 能否表达你需要的程序？
- **正确性（correctness）**：进程、机器或网络出故障时，Dex 是否仍然正确？

<a id="expressiveness"></a>

## 表达能力

[表达能力证明](https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/expressiveness-proof.md)说明：一门带线程、锁、Timer 和取消的小型并发语言中，任何程序都能写成行为相同的 Dex Flow。证明的每一步都由计算机检查。完整论证见[论文](https://docs.superdurable.io/zh-Hans/papers/dex-expressiveness.pdf)。

[Workflow Patterns 评估](https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/workflow-patterns.md)按 43 个 control-flow Workflow Patterns 为 Dex 评级。研究者用这些模式比较各种 workflow 语言和引擎。每个评级都配有可运行的示例和集成测试。

<a id="correctness"></a>

## 正确性

[Step 的保证](https://docs.superdurable.io/zh-Hans/concepts/step.md#guarantees)说明 Step 方法失败或重复运行时 Dex 的承诺。

[故障透明性证明](https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/failure-transparency-proof.md)覆盖 server 崩溃、备用 server 接管、重试、Dex 放弃后仍在运行的 Worker，以及重复的结果。这些故障只会带来重复的外部副作用：去掉它们，剩下的就是这个 Flow 在没有故障时能产生的事件序列。对公平的运行，结局也不变。证明的页面列出了它的条件，例如只覆盖 **SYNC** 方法、重试不会用完。这个证明同样经计算机检查，完整论证见同一篇[论文](https://docs.superdurable.io/zh-Hans/papers/dex-expressiveness.pdf)。

两个证明合起来，覆盖那门小型并发语言中每个格式良好的程序。这样的程序在 Dex 上产生的是一次无故障运行的事件，只是外部副作用可能重复，重复也可能来得很晚。[这对你的代码意味着什么](https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/failure-transparency-proof.md#what-it-means-for-you)说明怎样让重复变得安全。