Resolve message attributes in message types

[senier]

When substituting message types we currently ignore Message'First, Message'Last and Message'Size completely. This results in invalid specifications with inner expressions referring to outer message attributes.

To resolve this issue we will

• Substitute Message'Size by Message'Last - Message'First + 1
• Substitute Message'First by Field'First where Field is the first field of the inner message
• Substitute Message'Last by the Field'Last where Field is the last field of the inner message (on the respective path).
• Check that Field leads to final if Message'Last is used in the message type

In addition we should enforce #555 to make sure message are valid.