In the recent meeting with Kohei and Aybek, we also touched on how assertions could be introduced to the protocol notation.
There may be different levels of assertion, that record local state, facts (or commitments) and test them, However this initial notation will simply provide a way to test an assertion, using a 'require' term, based on state known through previous interactions.
The three statements that will be affected are:
1) The interaction
m:MsgType from A to B require <expr>;
The changes introduce the means of labelling a message to enable it to be referenced in an assertion expression. The actual expression language has not been agreed yet.
2) The choice
choice from A to B {
op(m:MsgType) require <expr>:
I1;
I2;
.....
}
3) The try/catch statement
try {
....
} catch(m:MsgType from A to B require <expr>) {
...
}
NOTE: In all of these situations, the 'require' expression (representing the assertion), is always tested at the sender.
