Different syntax for package separator and field access

[treiher]

Currently, . is used for two different actions in our specification:

• Qualifying types and literals imported from another package
• Accessing message fields

This makes it harder for a reader of the specification to differentiate the meaning of such a construct.

A similar question was already raised in #91, but we decided to keep the dot notation. As we are now integrating support for sessions, I would like to reconsider this decision.

Options

. / . (current syntax; similar to Ada, Python, ...)

      state NETWORK_IN_CONTENT is
      begin
         Plaintext := GreenTLS.Content'(Data => TLS_Record_Message.Fragment);
      transition
         then ERROR_INTERNAL_ERROR
            if Plaintext'Valid = False
         then NETWORK_IN_HANDSHAKE
            if TLS_Record_Message.Tag = TLS_Record.HANDSHAKE
         then NETWORK_IN_ALERT
            if TLS_Record_Message.Tag = TLS_Record.ALERT
         then ERROR_INTERNAL_ERROR
      end NETWORK_IN_CONTENT;

:: / . (similar to C++, Rust)

      state NETWORK_IN_CONTENT is
      begin
         Plaintext := GreenTLS::Content'(Data => TLS_Record::Message.Fragment);
      transition
         then ERROR_INTERNAL_ERROR
            if Plaintext'Valid = False
         then NETWORK_IN_HANDSHAKE
            if TLS_Record::Message.Tag = TLS_Record::HANDSHAKE
         then NETWORK_IN_ALERT
            if TLS_Record::Message.Tag = TLS_Record::ALERT
         then ERROR_INTERNAL_ERROR
      end NETWORK_IN_CONTENT;

\ / -> (similar to PHP)

      state NETWORK_IN_CONTENT is
      begin
         Plaintext := GreenTLS\Content'(Data => TLS_Record\Message->Fragment);
      transition
         then ERROR_INTERNAL_ERROR
            if Plaintext'Valid = False
         then NETWORK_IN_HANDSHAKE
            if TLS_Record\Message->Tag = TLS_Record\HANDSHAKE
         then NETWORK_IN_ALERT
            if TLS_Record\Message->Tag = TLS_Record\ALERT
         then ERROR_INTERNAL_ERROR
      end NETWORK_IN_CONTENT;