0 Replies Latest reply: Nov 27, 2010 5:05 PM by Gary Brown RSS

Level 1 assertions in protocol notation

Gary Brown Master

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.