overturetool
Imported definitions sometimes have the wrong type information
The following spec gives an incorrect warning:
module A
exports all
definitions
values
PERCENT: set1 of nat = {0,...,100};
end A
module B
imports from A values PERCENT renamed PERCENT;
exports all
definitions
types
T1 = nat
inv t == (exists p in set PERCENT & p = t); -- Empty set used in Bind for PERCENT here
end B
Warning 5009: Empty set used in bind in 'B' (test.vdm) at line 16:35
This is because the imported definition is a clone of the original export, not a reference to it (as Overture's AST requires). So when the definition in A is type-resolved, that does not update the imported/renamed definition in B. Subsequently it treats PERCENT as an unknown type, which in the bind context looks like it could possibly be an empty set.
It ought to be possible to avoid the warning by explicitly re-stating the type of the import:
...
imports from A values PERCENT : set1 of nat renamed PERCENT;
...
But that currently fails too. That is because import/renames ignore the stated type, giving preference to the type of the definition referred to - though as above, that isn't working in some cases. I will push a small fix to allow these explicit re-stated types to take effect. That does not fix the underlying problem, but it gives us a work-around to avoid the warning.