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

    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>:







      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.