cubesatlab / cubedos

A flight software framework in SPARK/Ada
48 stars 5 forks source link

Mercury should allow constant expressions in places where constants are currently expected #56

Open pchapin opened 4 months ago

pchapin commented 4 months ago

There are various places in Mercury's grammar where constants are expected, for example in range constraints (to mention one such place). Mercury should probably be extended to allow some form of "constant expression" to be used in many (most? all?) of those places. For example, consider this code:

typedef int T1 range 1 .. 10;
typedef int T2 range 1 .. 2 * T1'Last;  // Currently not allowed.

This would allow the specifier to indicate relationships between ranges using appropriate expressions rather than hard coding computed values. The result would be a more maintainable specification.

This is a significant change because it will require defining some notion of constant expression and, of course, extended Mercury to recognize and probably evaluate such expressions during processing.