How do we handle failure / divergence properly?
Opened this issue · 2 comments
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...
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).
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.