Confusing issue with "old"

[MikaelMayer]

Follow-up from #542

• old should not be accepted in preconditions.
• old should not be accepted in postconditions except if the variable is in the modifies clause.

Subject to more design reviews

• Procedures should declare all the global identifiers they read.