执行在绑定类型的存在

Question

考虑两个函数定义

test1 (x:nat) res:set of nat 
    == { m | m:nat & m in set {0,...,x} }; 

    test2 (x:nat) res:set of nat 
    == { m | m in set {0,...,x} & true }; 

运行在序曲TEST2（1000）给出了自然数的集合到1000运行TEST1（1000）给出了自然数集高达255.我明白，当明确的函数定义中有明确的类型绑定时会有复杂性，但在这种情况下，它只是默默地给出了错误的答案。看起来，当定义中出现自然数的类型绑定时，范围限制为0..255。至少，这似乎是从外面发生的事情。

章语言手册指出的8“注意，类型结合只能由VDM口译的情况下，上式可推导为有限静态地执行。”对于什么时候该类型可以被推断为静态有限是否有任何规则？

Answer 1

我现在这种行为是序曲的功能，我不知道敢肯定。默认情况下，该解释无法处理类型结合的无限类型，但在“调试”启动选项卡上的选项，允许数值类型结合（INT，NAT，NAT1和奇怪的是，真正的），以扩大从一系列的整数值“minint”改为“maxint”。您还必须勾选“numeric_type_bind_generation”框以启用该功能。

所以我对前面的混乱很抱歉。我不认为这个功能特别有用，我从来没有听说过任何人使用它，但我很确定它解释了你所看到的。

Answer 2

我不知道这里发生了什么你。当我尝试此规范与Overture的2.3.0（以及2.3.1快照和VDMJ）的test1的功能总是失败，立即说：

Error 4: Cannot get bind values for type nat 

你运行这个测试作为一个更大的规范的一部分？该手册是正确的。 Overture不能执行类型绑定，除非它可以确定类型是有限的，比如“bool”，或者完全由有限类型组成的东西，比如“set bool”或者“map P to Q”，其中P和Q是有限的。

基本有限类型是布尔和所有报价类型。然后这些类型可以用类型构造函数 - “set”构建更复杂的类型。除了“seq of”之外，所有类型构造函数只要所有成员类型都是有限的，就会产生有限类型。请注意，这包括[可选]类型，产品类型（如A * B），类型联合（如A | B | C）和记录构造函数。