1

考虑两个函数定义

  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 };

在 Overture 中运行 test2(1000) 给出的自然数集最多为 1000。运行 test1(1000) 给出的自然数集合最多为 255。我知道在显式函数定义中存在显式类型绑定时会出现复杂情况，但在这种情况下它只是默默地给出了错误的答案。似乎当自然数的类型绑定出现在定义中时，范围被限制为 0..255。至少，这似乎是从外面发生的事情。

语言手册的第 8 章指出“请注意，类型绑定只能由 VDM 解释器执行，以防可以静态推断类型是有限的。” 对于何时可以静态推断为有限类型是否有任何规则？

4

2 回答 2

1

我现在很确定这种行为是我不知道的 Overture 的一个功能。默认情况下，解释器无法处理无限类型的类型绑定，但在“调试器”启动器选项卡中有一个选项允许数字类型绑定（int、nat、nat1 和奇怪的是 real）扩展到从“minint”到“maxint”。您还必须勾选“numeric_type_bind_generation”框以启用该功能。

所以我很抱歉之前的混乱。我不认为这个功能特别有用，而且我从未听说有人使用它，但我很确定它解释了你所看到的。

于 2016-02-18T08:56:54.657 回答
1

我不确定这里发生了什么。当我使用 Overture 2.3.0（以及 2.3.1 快照和 VDMJ）尝试此规范时，test1 函数总是立即失败，并说：

Error 4: Cannot get bind values for type nat

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

基本的有限类型是 bool 和所有引号类型。然后，这些类型可用于使用类型构造函数（“set of”等）构建更复杂的类型。只要所有成员类型都是有限的，除了“seq of”之外，所有类型构造函数都将产生有限类型。请注意，这包括 [可选] 类型、产品类型（如 A*B）、类型联合（如 A|B|C）和记录构造函数。

于 2016-02-15T09:40:58.370 回答