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.