mach.int 库是 why3 的默认部分吗？

Question

我试图在 Simulink 模型的 Why3 规范中使用 32 位整数，我找到了 mach.int library, that is, at least in one place, described as being part of the standard library。但是，当我尝试将它与以下导入命令一起使用时：

  use import mach.int.Int32

我收到消息：

Library file not found: mach.int

这是我的第一个带有“.”的图书馆。在里面，所以我不确定我的语法是否错误，或者这个库实际上不是标准库的一部分，或者我是否做错了什么。

mach.int.Int32模块的正确使用方法是什么？

其他详细信息

我的why3版本是0.87.3:

▶ why3 --version
Why3 platform, version 0.87.3

我查看了我的 ~/.why3.conf 文件并找到了这些行：

[main]
loadpath = "/opt/gps/share/why3/theories"
loadpath = "/opt/gps/share/why3/modules"
loadpath = "/opt/gps/share/spark/theories"

我查看了 /opt/gps/share/why3/modules（以及 /opt/gps/share/why3/theories 和 /opt/gps/share/spark/theories）并没有找到 mach.int.*，所以我在 [=18] 中创建了一个 mach.int.mlw 文件=]，并确保 why3 可以接受：

▶ why3 prove -P z3 mach.int.mlw        
mach.int.mlw Int WP_parameter infix / : Valid (0.01s)
mach.int.mlw Int WP_parameter infix % : Valid (0.01s)
mach.int.mlw Refint63 WP_parameter incr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter decr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix += : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix -= : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix *= : Valid (0.02s)
mach.int.mlw MinMax63 WP_parameter min : Valid (0.01s)
mach.int.mlw MinMax63 WP_parameter max : Valid (0.02s)

结果是一样的

Answer 1

事实证明，why3 在 mach 子目录的模块 int.mlw 中寻找 mach.int.Int32。

将 mach.int library 放入 /opt/gps/share/why3/modules/mach/ 目录解决了找不到库的问题（其中 /opt/gps/share/why3/modules 在我的 [= 中被定义为 loadpath 的一部分17=] 文件).

mach.int 库是 why3 的​​默认部分吗？

Is the mach.int library a default part of why3?

why3

其他详细信息

mach.int 库是 why3 的默认部分吗？