无需规范的细化

<p>假设我们有一个SQL数据库，其中包含一个<code>user</code>表，用户有一个不可为空的<code>is_activated</code>布尔列。在阅读了<a href="https://ntietz.com/blog/that-boolean-should-probably-be-something-else/" target="_blank">那个布尔值很可能应该是别的东西</a>之后，你决定将其迁移到一个可空的<code>activated_at</code>列。你可以更改任何读取/更新<code>user</code>表的SQL查询，但不能更改使用这些查询结果的代码。我们能否以一种保留所有外部属性的方式进行这种更改？ </p> <p>是的。如果一个更新会将<code>is_activated</code>设置为true，则改为将其设置为当前日期。现在定义<strong>细化映射</strong>，它接受一个<code>new_user</code>并返回一个<code>old_user</code>。所有列将保持不变<em>除了</em><code>is_activated</code>，它将变为</p> <div class="codehilite"><pre><span></span><code>f(new_user).is_activated = if new_user.activated_at == NULL then FALSE else TRUE </code></pre></div> <p>现在新代码可以直接使用<code>new_user</code>，而旧代码可以使用<code>f(new_user)</code>，其行为与<code>old_user</code>无法区分。 </p> <p>过了一段时间，你决定切换到一个类似<a href="https://martinfowler.com/eaaDev/EventSourcing.html" target="_blank">事件溯源</a>的模型。因此，不再使用<code>activated_at</code>列，而是使用一个<code>user_events</code>表，其中每条记录是<code>(user_id, timestamp, event)</code>。所以添加一个<code>activate</code>事件将激活用户，添加一个<code>deactivate</code>事件将停用用户。同样，我们可以更新查询，但不能更改使用这些查询结果的任何代码。我们能否进行一种保留所有外部属性的更改？</p> <p>是的。如果一个更新会改变<code>is_activated</code>，则改为在事件表中添加一条适当的记录。现在，定义细化映射，它接受<code>newer_user</code>并返回<code>new_user</code>。<code>activated_at</code>字段将按如下方式计算：</p> <div class="codehilite"><pre><span></span><code>g(newer_user).activated_at = # last_activated_event let lae = newer_user.events .filter(event = &quot;activate&quot; | &quot;deactivate&quot;) .last, in if lae.event == &quot;activate&quot; then lae.timestamp else NULL </code></pre></div> <p class="empty-line" style="height:16px; margin:0px !important;"></p> <p>现在新代码可以直接使用<code>newer_user</code>，旧代码可以使用<code>g(newer_user)</code>，而非常旧的代码可以使用<code>f(g(newer_user))</code>。</p> <h3>可变性约束</h3> <div class="subscribe-form"></div> <p>我之前说“这些保留了所有外部属性”，但那是说谎。这取决于我们明确拥有的属性，而我没有列出任何属性。对我来说，真正有趣的属性是关于系统如何演化的可变性约束。所以让我们回到过去，为<code>user</code>添加一个约束：</p> <div class="codehilite"><pre><span></span><code>C1(u) = u.is_activated =&gt; u.is_activated&#39; </code></pre></div> <p>这个约束意味着如果一个用户被激活，任何更改都将保持其激活状态。这意味着一个用户可以从停用变为激活，但不能反过来。这不是一个特别好的约束，但足以用于教学目的。这种SQL约束可以通过<a href="https://www.postgresql.org/docs/current/sql-createeventtrigger.html" target="_blank">触发器</a>来强制执行。 </p> <p>现在我们可以对<code>new_user</code>施加一个约束：</p> <div class="codehilite"><pre><span></span><code>C2(nu) = nu.activated_at != NULL =&gt; nu.activated_at&#39; != NULL </code></pre></div> <p>如果<code>nu</code>满足<code>C2</code>，那么<code>f(nu)</code>满足<code>C1</code>。因此细化仍然成立。</p> <p>对于<code>newer_u</code>，我们<em>不能</em>保证<code>g(newer_u)</code>满足<code>C2</code>，因为我们可以通过追加一个新事件从“激活”变为“停用”。所以这不是一个细化。这可以通过移除停用事件来修复，那样也行。</p> <p>所以一个更有趣的情况是<code>bad_user</code>，它是<code>user</code>的一个细化，同时具有<code>activated_at</code>和<code>activated_until</code>。我们提出细化映射<code>b</code>：</p> <div class="codehilite"><pre><span></span><code>b(bad_user).activated = if bad_user.activated_at == NULL &amp;&amp; activated_until == NULL then FALSE else bad_user.activated_at &lt;= now() &lt; bad_user.activated_until </code></pre></div> <p>但现在如果经过足够的时间，<code>b(bad_user).activated' = false</code>，所以这也不是一个细化。</p> <h3>点睛之笔</h3> <p>细化是形式化规范中最强大的技术之一，但也是最难理解的技术之一。我开始认为它之所以如此困难，是因为人们在<em>同时</em>学习形式化方法时学习细化，因此在一个陌生的环境中面对一个陌生的话题。如果是这样，那么也许在像数据库这样更常见的上下文中引入细化会更容易。</p> <p>我曾在<a href="https://hillelwayne.com/post/refinement/" target="_blank">这里</a>写过一些关于正常上下文中细化的内容（展示一个规范是另一个规范的实现）。我有点想把这种解释写进书里，但可能已经太晚了，不适合做这样大的内容补充。</p> <p>（思考：细化映射与数据库视图有何关系？）</p>