证明可能性

<p>作为一名形式化方法顾问，我需要用数学方式表达系统的性质。我通常使用两个"时序算子"来完成这项工作：</p> <ul> <li>A(x) 表示 <code>x</code> 总是成立。例如，数据库表<em>总是</em>满足所有记录级约束，状态机<em>总是</em>在状态间进行有效转换。如果 <code>x</code> 是关于单个状态的陈述（如数据库示例，而非状态机示例），我们进一步称其为<strong>不变量</strong>。</li> <li>E(x) 表示 <code>x</code> "最终"成立，通常指"在未来的某个时刻必然成立"。数据库事务<em>最终</em>要么完成要么回滚，状态机<em>最终</em>到达"完成"状态，等等。</li> </ul> <p>这些算子来自线性时序逻辑，该逻辑是表述系统性质的主流符号体系。<sup id="fnref:modal"><a class="footnote-ref" href="#fn:modal">1</a></sup> 我们喜欢这些算子，因为它们简洁地涵盖了<a href="https://www.hillelwayne.com/post/safety-and-liveness/" target="_blank">安全性和活性性质</a>，并且<a href="https://buttondown.com/hillelwayne/archive/formalizing-stability-and-resilience-properties/" target="_blank">我们可以组合使用它们</a>。<code>A(E(x))</code> 表示 <code>x</code> 无限次成立，而 <code>A(x =&gt; E(y))</code> 表示 <code>x</code> 成立能保证 <code>y</code> 在将来成立。</p> <p>还有第三类性质，我称之为<em>可能性</em>性质：<code>P(x)</code> 表示"<code>x</code> 在这个模型中可能发生吗？" 一个表格可能拥有超过十条记录吗？一个状态机能否从"完成"状态转换到"重试"状态，即使它<em>实际上</em>并不这么转换？重要的是，<code>P(x)</code> 并不需要<em>立即</em>可能，只需在未来某个时刻可能。即使你每次只赌一美元，老虎机也有可能让你输掉一百美元。如果 <code>x</code> 是关于单个状态的陈述，我们可以进一步称其为<a href="https://en.wikipedia.org/wiki/Reachability" target="_blank"><em>可达性</em>性质</a>。为行文流畅，我将二者混用。</p> <p><code>A(P(x))</code> 表示 <code>x</code> <em>总是</em>可能的。无论我们在系统中做了什么，我们都能让 <code>x</code> 再次发生。仅靠 <code>A</code> 和 <code>E</code> 无法做到这一点。其他有意义的组合包括：</p> <ul> <li><code>P(A(x))</code>：存在一个可达状态，从该状态起 <code>x</code> 总是成立。</li> <li><code>A(x =&gt; P(y))</code>：从任何 <code>x</code> 成立的状态出发，<code>y</code> 都是可能的。</li> <li><code>E(x &amp;&amp; P(y))</code>：总是存在一个未来状态，其中 <code>x</code> 成立且 <code>y</code> 可达。</li> <li><code>A(P(x) =&gt; E(x))</code>：如果 <code>x</code> 是可能的，那么它最终会发生。</li> <li><code>E(P(x))</code> 和 <code>P(E(x))</code> 等同于 <code>P(x)</code>。</li> </ul> <p>有关 <code>E</code> 和 <code>P</code> 的深入讨论，请参阅论文 <a href="https://dl.acm.org/doi/epdf/10.1145/567446.567463" target="_blank">"Sometime" is sometimes "not never"</a>。</p> <h3>使用场景</h3> <p>可能性性质表示"好事<em>可以</em>发生"，通常（在规约中）不如"坏事<em>不能</em>发生"（安全性）和"好事<em>会</em>发生"（活性）那么有用。但它仍然是一项重要性质！我最喜欢的例子：</p> <p><img alt="一个因为系统偏好设置中断关机而无法关闭电脑的人" class="newsletter-image" src="https://www.hillelwayne.com/post/safety-and-liveness/img/tweet2.png" /></p> <p>我发现这个概念的主要用途是作为合理性检查，确认我们正确编写了规约。例如，考虑性质"处于'重试'状态的工人最终会离开该状态"：</p> <div class="codehilite"><pre><span></span><code>A(state == &#39;Retry&#39; =&gt; E(state != &#39;Retry&#39;)) </code></pre></div> <p>模型检查器检查该性质并确认它在规约中成立。太棒了！我们的系统是正确的！……除非系统永远无法<em>到达</em>"重试"状态，此时该表达式是平凡成立的。我需要验证'Retry'是可达的，例如 <code>P(state == 'Retry')</code>。注意，我不能用 <code>E</code> 来做这件事，因为我并不想说"工人必须至少重试一次"。</p> <h3>但工具并不支持</h3> <p>我说"我发现<em>这个概念</em>的用途"，是因为我主要使用的形式化方法工具（Alloy 和 TLA+）本身并不支持 <code>P</code>。<sup id="fnref:tla"><a class="footnote-ref" href="#fn:tla">2</a></sup> 除了 <code>P</code> 不如 <code>A</code> 和 <code>E</code> 有用之外，简单的可达性性质可以通过 <code>A(x)</code> <a href="https://www.hillelwayne.com/post/software-mimicry/" target="_blank">模拟</a>。当 <code>A(!x)</code> <em>失败</em>时，<code>P(x)</code> 就<em>通过</em>了，这意味着我可以通过测试 <code>A(!(state == 'Retry'))</code> 是否找到反例来验证 <code>P(state == 'Retry')</code>。但我们不能用这种方式模拟组合算子如 <code>A(P(x))</code>，不过这类算子远不如状态可达性常见。</p> <p>（此外，精化不保持可能性性质，但这完全是另一码事。）</p> <p>有一点让我略感头疼：我们无法模拟"从每个起始状态出发 <code>P(x)</code> 成立"。"<code>A(!x)</code>" 只要存在一条从某个起始状态出发的路径能到达 <code>x</code> 就会失败，但其他起始状态可能无法使 <code>x</code> 成为可能。</p> <p>我怀疑这里还存在一个先有鸡还是先有蛋的问题。由于我的工具无法验证可能性性质，我并不习惯在系统中注意到它们。我很想知道是否有人处理过代码库中可能性性质很重要的情况，特别是像 <code>A(x =&gt; P(y))</code> 这样复杂的组合。</p> <div class="footnote"> <hr /> <ol> <li id="fn:modal"> <p>文献中通常用 <code>[]x</code> 或 <code>Gx</code>（"globally x"）代替 <code>A(x)</code>，用 <code>&lt;&gt;x</code> 或 <code>Fx</code>（"finally x"）代替 <code>E(x)</code>。此处使用 A 和 E 并非教学目的。&#160;<a class="footnote-backref" href="#fnref:modal" title="回到脚注 1">&#8617;</a></p> </li> <li id="fn:tla"> <p>关于在 TLA+ 中添加该算子的讨论，参见<a href="https://github.com/tlaplus/tlaplus/issues/860" target="_blank">此处</a>。&#160;<a class="footnote-backref" href="#fnref:tla" title="回到脚注 2">&#8617;</a></p> </li> </ol> </div>