VDMJ produces a warning if you define types with order or equality clauses and then combine them in a union that has its own order or equality clause. For example:
types
T1 = nat
ord a < b == a < b;
T2 = nat;
U = T1 | T2 <--- Warning 5019: Order of union member T1 will be overridden
ord a < b == b < a;
VDMJ produces a warning if you define types with order or equality clauses and then combine them in a union that has its own order or equality clause. For example:
These are missing from Overture 2.7.4.