在存在类型绑定时执行

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和奇怪的是，the )扩展到从"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

您是否将此测试作为更大规范的一部分运行？手册是正确的。除非能确定类型是有限的，如" bool“，或者完全由有限类型组成的东西，如”bool集“或”映射P到Q“，否则序曲不能执行类型绑定，其中P和Q是有限的。

基本的有限类型是bool和所有的引用类型。然后，这些类型可以使用类型构造函数-- "set of“等来构建更复杂的类型。所有类型的构造函数，除了"seq of"，只要所有成员类型都是有限的，就会产生有限的类型。请注意，这包括可选类型、产品类型(如A*B )、类型联合(如A+B)、以及记录构造函数( record constructors )。