How do we handle failure / divergence properly?

[septract]

Right now in the Starling input language, we can't write partial commands, eg. assert(x==1) or similar. This is because Starling's two-state representation doesn't have a way of expressing command failure: if a pre-state isn't defined, this is interpreted as divergence.

It's not clear what the semantics of failure should be. Perhaps we should map the pre-state to all post-states, i.e. model it as havoc? Do we need an explicit failure state? We should probably talk to the UTP people about this...

[MattWindsor91]

In the UTP world I think this is generally handled with a special variable ok that is supposed to be held true always (and setting it to false models nontermination/divergence).

[MattWindsor91]

As per what I said in #123, what I think we could do is add a directive, something like

with assert;

which will desugar (once we have custom command semantics, which is probably not quite in scope yet) to

shared bool ok; // fresh name?
constraint emp -> ok; // conjoins with existing emp
command assert(bool condition) { ok <- condition; }
command error() { ok <- false; }

This seems like it'd be the least theoretically nauseous way of doing this. (Ideally I'd want this to be opt-in, so that 'ok' and the emp constraint on it don't appear in proofs of non-failing programs).

For now we'd probably have assert and error as native commands.