We introduce a new construct \(\texttt {fail}\) which denotes the failure state, as an alternative to \(\sigma \).

For the assumption we only have a \(\top \) rule, the idea being if the assumption holds then the statement is equivalent to a \(\texttt {skip}\) otherwise the execution gets stuck but doesn't fail.

The idea with getting stuck being that since we aren't failing for the case of partial-correctness (failure or termination) it means we can simply ignore this case.

The final big-step evaluation rule is for the havoc statement:

In addition to our big-step evaluation rules we also have Hoare rules.

A central thing to understand with assertions especially is that they integrate a result's monad into the big-step evaluation semantics, in addition to the Hoare logic. So the idea is now instead of the relationship being denoted by:

It's now expressed as

Where we can model \(\texttt {Result}\) as the following monad

    inductive Result (α : Type)
    | ok : α → Result α      -- Normal termination with final state
    | fail : Result α        -- Assertion failure / error state
    deriving Repr, DecidableEq
  

At this point if you want to be pedantic it's worth mentioning that the implication is that we are lifting all other inference rules into the context of this result monad, though for pedagogical purposes its enough to just assume that \(\Downarrow \sigma \) just corresponds to \(\Downarrow \texttt {.ok} \sigma \) i.e. evaluated into a non-fail state.

The Hoare triple is where stuff becomes a bit more interesting. As a reminder, the classical hoare triple is basically just an alias for the logical formula:

Naturally because we know are no longer evaluating into just \(\sigma '\) but either an \(\texttt {ok}\) or \(\texttt {fail}\) state, it's worth asking how we actually represent that as a Hoare triple. We can start in much the same way as we do for the regular partial correctness hoare triple

Here we then run into I guess a design choice as to how we proceed, the two main possibilities are:

• We fail sometimes succeed other times this would mean that: \[ (\exists \sigma ', \sigma _t = \texttt {.ok}\ \sigma ' \land Q(\sigma ')) \] another way of seeing this is here we are disallowig failure meaning that for a hoare triple to be proven valid we must explicitly demonstrate as a side condition that we cannot fail otherwise our hoare triple is invalid.
• We never fail which would mean that: \[ (\forall \sigma ', \sigma _t = \texttt {.ok}\ \sigma ' \land Q(\sigma ')) \] for this rule another way of seeing it is we are ignoring failure or filter success states since we are clearly only quantifying over those states that are successfull.

The latter option seems to be generally more common in theoretical settings because it doesn't require explicitly accounting for failure states, they are just implicitly filtered out in the logic.