0

我正在尝试在 Simulink 模型的 Why3 规范中使用 32 位整数，并且我找到了mach.int 库，也就是说，至少在一个地方，它被描述为标准库的一部分。但是，当我尝试将它与以下导入命令一起使用时：

  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(and /opt/gps/share/why3/theoriesand /opt/gps/share/spark/theories) 并发现 no mach.int.*，所以我在 中创建了一个mach.int.mlw文件/opt/gps/share/why3/modules，并确保它没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)

结果是一样的。

4

1 回答 1

0

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

将mach.int库放在/opt/gps/share/why3/modules/mach/目录中解决了找不到库的问题（在我的文件/opt/gps/share/why3/modules中定义为其中的一部分）。loadpath~/.why3.conf

于 2017-07-27T23:05:05.173 回答