Refinement without Specification

<p>Imagine we have a SQL database with a <code>user</code> table, and users have a non-nullable <code>is_activated</code> boolean column. Having read <a href="https://ntietz.com/blog/that-boolean-should-probably-be-something-else/" target="_blank">That Boolean Should Probably Be Something else</a>, you decide to migrate it to a nullable <code>activated_at</code> column. You can change any of the SQL queries that read/update the <code>user</code> table but not any of the code that uses the results of these queries. Can we make this change in a way that preserves all external properties? </p> <p>Yes. If an update would set <code>is_activated</code> to true, instead set it to the current date. Now define the <strong>refinement mapping</strong> that takes a <code>new_user</code> and returns an <code>old_user</code>. All columns will be unchanged <em>except</em> <code>is_activated</code>, which will be</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>Now new code can use <code>new_user</code> directly while legacy code can use <code>f(new_user)</code> instead, which will behave indistinguishably from the <code>old_user</code>. </p> <p>A little more time passes and you decide to switch to an <a href="https://martinfowler.com/eaaDev/EventSourcing.html" target="_blank">event sourcing</a>-like model. So instead of an <code>activated_at</code> column, you have a <code>user_events</code> table, where every record is <code>(user_id, timestamp, event)</code>. So adding an <code>activate</code> event will activate the user, adding a <code>deactivate</code> event will deactivate the user. Once again, we can update the queries but not any of the code that uses the results of these queries. Can we make a change that preserves all external properties?</p> <p>Yes. If an update would change <code>is_activated</code>, instead have it add an appropriate record to the event table. Now, define the refinement mapping that takes <code>newer_user</code> and returns <code>new_user</code>. The <code>activated_at</code> field will be computed like this:</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>Now new code can use <code>newer_user</code> directly while old code can use <code>g(newer_user)</code> and the really old code can use <code>f(g(newer_user))</code>.</p> <h3>Mutability constraints</h3> <div class="subscribe-form"></div> <p>I said "these preserve all external properties" and that was a lie. It depends on the properties we explicitly have, and I didn't list any. The real interesting properties for me are mutability constraints on how the system can evolve. So let's go back in time and add a constraint to <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>This constraint means that if a user is activated, any change will preserve its activated-ness. This means a user can go from deactivated to activated but not the other way. It's not a particular good constraint but it's good enough for teaching purposes. Such a SQL constraint can be enforced with <a href="https://www.postgresql.org/docs/current/sql-createeventtrigger.html" target="_blank">triggers</a>. </p> <p>Now we can throw a constraint on <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>If <code>nu</code> satisfies <code>C2</code>, then <code>f(nu)</code> satisfies <code>C1</code>. So the refinement still holds.</p> <p>With <code>newer_u</code>, we <em>cannot</em> guarantee that <code>g(newer_u)</code> satisfies <code>C2</code> because we can go from "activated" to "deactivated" just by appending a new event. So it's not a refinement. This is fixable by removing deactivation events, that would work too.</p> <p>So a more interesting case is <code>bad_user</code>, a refinement of <code>user</code> that has both <code>activated_at</code> and <code>activated_until</code>. We propose the refinement mapping <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>But now if enough time passes, <code>b(bad_user).activated' = false</code>, so this is not a refinement either.</p> <h3>The punchline</h3> <p>Refinement is one of the most powerful techniques in formal specification, but also one of the hardest for people to understand. I'm starting to think that the reason it's so hard is because they learn refinement while they're <em>also</em> learning formal methods, so are faced with an unfamiliar topic in an unfamiliar context. If that's the case, then maybe it's easier introducing refinement in a more common context like databases.</p> <p>I've written a bit about refinement in the normal context <a href="https://hillelwayne.com/post/refinement/" target="_blank">here</a> (showing one specification is an implementation of another). I kinda want to work this explanation into the book but it might be too late for big content additions like this.</p> <p>(Food for thought: how do refinement mappings relate to database views?)</p>