Currently message invariants allow for only very limited expression forms. The feature would be more useful if the expression language supported was richer. In particular, logical connectives ('and', 'or', 'not') should be supported so that multiple expressions can be combined in conjunctions, etc. This would allow the "feature" of supporting multiple invariants to be removed and, by so doing, simplify the mapping to SPARK postconditions.
Currently message invariants allow for only very limited expression forms. The feature would be more useful if the expression language supported was richer. In particular, logical connectives ('and', 'or', 'not') should be supported so that multiple expressions can be combined in conjunctions, etc. This would allow the "feature" of supporting multiple invariants to be removed and, by so doing, simplify the mapping to SPARK postconditions.